English
In a second-countable space, any generating family for the topology has a countable generating subfamily.
Русский
В пространстве с двойной счетностью любая подсистема порождает ту же топологию; существует счетное подмножество порождающее топологию.
LaTeX
$$$\forall t:\Set(Set α),\; ts = generateFrom t \Rightarrow ∃ s ⊆ t, s.Countable ∧ ts = generateFrom s$$$
Lean4
/-- In a second countable topological space, any family generating the topology admits a
countable generating subfamily. -/
theorem exists_countable_of_generateFrom {α : Type*} [ts : TopologicalSpace α] [SecondCountableTopology α]
{t : Set (Set α)} (ht : ts = generateFrom t) : ∃ s ⊆ t, s.Countable ∧ ts = generateFrom s :=
by
let t' := (fun f => ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
have : IsTopologicalBasis t' := TopologicalSpace.isTopologicalBasis_of_subbasis ht
obtain ⟨s', s't', s'_count, hs'⟩ : ∃ s' ⊆ t', s'.Countable ∧ IsTopologicalBasis s' := this.exists_countable
have A : ∀ u ∈ s', ∃ (f : Set (Set α)), f.Finite ∧ f ⊆ t ∧ ⋂₀ f = u := fun u hu ↦ by
simpa [t', and_assoc] using s't' hu
choose! f f_fin ft hf using A
refine ⟨⋃ u ∈ s', f u, by simpa using ft, ?_, ?_⟩
· apply s'_count.biUnion
intro u hu
exact Finite.countable (f_fin u hu)
· apply le_antisymm
· apply le_generateFrom_iff_subset_isOpen.2
simp only [iUnion_subset_iff]
intro u hu v hv
rw [ht]
apply isOpen_generateFrom_of_mem
exact ft u hu hv
· rw [hs'.eq_generateFrom]
apply le_generateFrom_iff_subset_isOpen.2
intro u hu
rw [← hf u hu, sInter_eq_biInter]
change IsOpen[generateFrom _] (⋂ i ∈ f u, i)
apply @Finite.isOpen_biInter _ _ (generateFrom (⋃ u ∈ s', f u)) _ _
· apply f_fin u hu
· intro i hi
apply isOpen_generateFrom_of_mem
simp
grind
