English
In a second-countable space, any topological basis contains a countable subset forming a basis.
Русский
Во втором счётном пространстве существует счётное подмножество базиса, которое образует базис.
LaTeX
$$$[SecondCountableTopology\ α] \{t : Set(Set α)\} (ht : IsTopologicalBasis t) : ∃ s ⊆ t, s.Countable ∧ IsTopologicalBasis s$$$
Lean4
/-- In a second countable topological space, any topological basis contains a countable subset
which is also a topological basis. -/
theorem exists_countable [SecondCountableTopology α] {t : Set (Set α)} (ht : IsTopologicalBasis t) :
∃ s ⊆ t, s.Countable ∧ IsTopologicalBasis s :=
by
have A : ∀ u ∈ countableBasis α, ∃ s ⊆ t, s.Countable ∧ u = ⋃ a ∈ s, a := fun u hu ↦
ht.exists_countable_biUnion_of_isOpen ((isBasis_countableBasis α).isOpen hu)
choose! s hst s_count hs using A
refine ⟨⋃ u ∈ countableBasis α, s u, by simpa using hst, (countable_countableBasis α).biUnion s_count, ?_⟩
apply isTopologicalBasis_of_isOpen_of_nhds
· simp only [mem_iUnion, exists_prop, forall_exists_index, and_imp]
have := @ht.isOpen
grind
· intro x v hx hv
simp only [mem_iUnion, exists_prop]
obtain ⟨u, u_mem, xu, uv⟩ : ∃ u ∈ countableBasis α, x ∈ u ∧ u ⊆ v := (isBasis_countableBasis α).isOpen_iff.1 hv _ hx
have : x ∈ ⋃ a ∈ s u, a := by
convert xu
exact (hs u u_mem).symm
obtain ⟨w, ws, xw⟩ : ∃ w ∈ s u, x ∈ w := by simpa using this
refine ⟨w, ⟨u, u_mem, ws⟩, xw, ?_⟩
apply Subset.trans (Subset.trans _ (hs u u_mem).symm.subset) uv
exact subset_iUnion₂_of_subset w ws (Subset.refl _)
