English
If a family of open sets s is such that every open neighborhood contains some member of s, then s is a topological basis.
Русский
Если семейство открытых множеств s таково, что каждое открытое окрестное множество содержит некоторый элемент из s, тогда s образует топологическую базу.
LaTeX
$$isTopologicalBasis_of_isOpen_of_nhds {s : Set (Set α)} (h_open : ∀ u ∈ s, IsOpen u) (h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v ∈ s, a ∈ v ∧ v ⊆ u) : IsTopologicalBasis s$$
Lean4
/-- If a family of open sets `s` is such that every open neighbourhood contains some
member of `s`, then `s` is a topological basis. -/
theorem isTopologicalBasis_of_isOpen_of_nhds {s : Set (Set α)} (h_open : ∀ u ∈ s, IsOpen u)
(h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v ∈ s, a ∈ v ∧ v ⊆ u) : IsTopologicalBasis s :=
.of_hasBasis_nhds <| fun a ↦
(nhds_basis_opens a).to_hasBasis' (by simpa [and_assoc] using h_nhds a) fun _ ⟨hts, hat⟩ ↦
(h_open _ hts).mem_nhds hat
