English
If t = generateFrom s and FiniteInter s, then s is a topological basis.
Русский
Если топология порождается s = generateFrom(s) и FiniteInter s выполняется, то s является базой.
LaTeX
$$isTopologicalBasis_of_subbasis_of_finiteInter {s : Set (Set α)} (hsg : t = generateFrom s) (hsi : FiniteInter s) : IsTopologicalBasis s$$
Lean4
theorem of_hasBasis_nhds {s : Set (Set α)} (h_nhds : ∀ a, (𝓝 a).HasBasis (fun t ↦ t ∈ s ∧ a ∈ t) id) :
IsTopologicalBasis s
where
exists_subset_inter t₁ ht₁ t₂ ht₂ x
hx := by
simpa only [and_assoc, (h_nhds x).mem_iff] using
(inter_mem ((h_nhds _).mem_of_mem ⟨ht₁, hx.1⟩) ((h_nhds _).mem_of_mem ⟨ht₂, hx.2⟩))
sUnion_eq := sUnion_eq_univ_iff.2 fun x ↦ (h_nhds x).ex_mem
eq_generateFrom := ext_nhds fun x ↦ by simpa only [nhds_generateFrom, and_comm] using (h_nhds x).eq_biInf
