English
In a second-countable space, any topological basis contains a countable subset which is also a basis.
Русский
Во второ-счетном пространстве любой базис содержит счётное подмножество, которое также образует базис.
LaTeX
$$$[SecondCountableTopology\ α] \{t : Set(Set α)\} (ht : IsTopologicalBasis t) : ∃ s ⊆ t, s.Countable ∧ IsTopologicalBasis s$$$
Lean4
/-- In a second countable topological space, any open set is a countable union of elements in a
given topological basis. -/
theorem exists_countable_biUnion_of_isOpen [SecondCountableTopology α] {t : Set (Set α)} (ht : IsTopologicalBasis t)
{u : Set α} (hu : IsOpen u) : ∃ s ⊆ t, s.Countable ∧ u = ⋃ a ∈ s, a :=
by
have A : ∀ x ∈ u, ∃ a ∈ t, x ∈ a ∧ a ⊆ u := fun x hx ↦ ht.exists_subset_of_mem_open hx hu
choose! a hat xa au using A
obtain ⟨T, T_count, hT⟩ : ∃ T : Set u, T.Countable ∧ ⋃ i ∈ T, a i = ⋃ (i : u), a i :=
by
apply isOpen_iUnion_countable _
rintro ⟨x, hx⟩
exact ht.isOpen (hat x hx)
refine ⟨(fun (x : u) ↦ a x) '' T, ?_, T_count.image _, ?_⟩
· simp only [image_subset_iff]
rintro ⟨x, xu⟩ -
exact hat x xu
rw [biUnion_image, hT]
apply Subset.antisymm
· intro x hx
simp
grind
· simp
grind
