English
If a topology is generated from a subbasis s, then finite intersections of subbasis elements form a topological basis.
Русский
Если топология порождается подбазисом s, то конечные пересечения элементов подбазиса образуют топологическую базу.
LaTeX
$$isTopologicalBasis_of_subbasis {s : Set (Set α)} (hs : t = generateFrom s) : IsTopologicalBasis ((fun f => ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s})$$
Lean4
/-- If a family of sets `s` generates the topology, then intersections of finite
subcollections of `s` form a topological basis. -/
theorem isTopologicalBasis_of_subbasis {s : Set (Set α)} (hs : t = generateFrom s) :
IsTopologicalBasis ((fun f => ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s}) :=
by
subst t; letI := generateFrom s
refine ⟨?_, ?_, le_antisymm (le_generateFrom ?_) <| generateFrom_anti fun t ht => ?_⟩
· rintro _ ⟨t₁, ⟨hft₁, ht₁b⟩, rfl⟩ _ ⟨t₂, ⟨hft₂, ht₂b⟩, rfl⟩ x h
exact ⟨_, ⟨_, ⟨hft₁.union hft₂, union_subset ht₁b ht₂b⟩, sInter_union t₁ t₂⟩, h, Subset.rfl⟩
· rw [sUnion_image, iUnion₂_eq_univ_iff]
exact fun x => ⟨∅, ⟨finite_empty, empty_subset _⟩, sInter_empty.substr <| mem_univ x⟩
· rintro _ ⟨t, ⟨hft, htb⟩, rfl⟩
exact hft.isOpen_sInter fun s hs ↦ GenerateOpen.basic _ <| htb hs
· rw [← sInter_singleton t]
exact ⟨{ t }, ⟨finite_singleton t, singleton_subset_iff.2 ht⟩, rfl⟩
