MathlibAnnex.Topology.HasDensityCharacter.of_cardinalMk_le_of_forall_dense

Exact source view. Private integrated preview.

Exact declaration: MathlibAnnex.Topology.HasDensityCharacter.of_cardinalMk_le_of_forall_dense

MathlibAnnex/Topology/DensityCharacter.lean · lines 43–48

Raw UTF-8 source

1import Mathlib.Topology.Bases
2import Mathlib.SetTheory.Cardinal.Continuum
3
4/-!
5# Exact density character
6
7`HasDensityCharacter X κ` means that κ is the attained minimum of cardinalities
8of dense subsets of X. In particular, it is not merely the existence of a dense
9subset with κ elements. For a normed space, the inherited topology is the norm
10topology. This interface avoids converting a generator-count statement into a
11density statement without proof.
12-/
13
14set_option autoImplicit false
15open Set
16open scoped Cardinal
17namespace MathlibAnnex.Topology
18universe u
19
20/-- The minimum cardinality of a dense subset of X is exactly κ. -/
21def HasDensityCharacter (X : Type u) [TopologicalSpace X] (κ : Cardinal.{u}) : Prop :=
22  (∃ s : Set X, Dense s ∧ #s = κ) ∧ ∀ s : Set X, Dense s → κ ≤ #s
23
24namespace HasDensityCharacter
25variable {X : Type u} [TopologicalSpace X] {κ μ : Cardinal.{u}}
26
27/-- The witnessing dense subset realizes the specified cardinal. -/
28theorem exists_dense (h : HasDensityCharacter X κ) :
29    ∃ s : Set X, Dense s ∧ #s = κ := h.1
30
31/-- Every dense subset has cardinality at least the density character. -/
32theorem le_cardinalMk (h : HasDensityCharacter X κ) (s : Set X) (hs : Dense s) :
33    κ ≤ #s := h.2 s hs
34
35/-- Exact density character is unique. -/
36theorem unique (hκ : HasDensityCharacter X κ) (hμ : HasDensityCharacter X μ) : κ = μ := by
37  obtain ⟨s, hs, hsc⟩ := hκ.1
38  obtain ⟨t, ht, htc⟩ := hμ.1
39  exact le_antisymm (htc ▸ hκ.2 t ht) (hsc ▸ hμ.2 s hs)
40
41/-- A cardinal upper bound on X and the matching bound on every dense subset
42identify both the cardinality and the density character. -/
43theorem of_cardinalMk_le_of_forall_dense
44    (hupper : #X ≤ κ) (hlower : ∀ s : Set X, Dense s → κ ≤ #s) :
45    HasDensityCharacter X κ := by
46  have hlow : κ ≤ #X := by simpa using hlower Set.univ dense_univ
47  have hcard : #X = κ := le_antisymm hupper hlow
48  exact ⟨⟨Set.univ, dense_univ, by simpa using hcard⟩, hlower⟩
49
50end HasDensityCharacter
51end MathlibAnnex.Topology