English
A collection B of opens is a basis if and only if for every open U and every point x in U there exists V in B with x ∈ V ⊆ U.
Русский
Множество открытых множеств является базисом тогда и только тогда, когда для любого открытого множества U и любого элемента x ∈ U существует V ∈ B с x ∈ V ⊆ U.
LaTeX
$$$\forall U \in \operatorname{Opens}(\alpha), \forall x (x \in U) \Rightarrow \exists V \in B, x \in V \land V \le U$$$
Lean4
theorem isBasis_iff_nbhd {B : Set (Opens α)} : IsBasis B ↔ ∀ {U : Opens α} {x}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U :=
by
constructor <;> intro h
· rintro ⟨sU, hU⟩ x hx
rcases h.mem_nhds_iff.mp (IsOpen.mem_nhds hU hx) with ⟨sV, ⟨⟨V, H₁, H₂⟩, hsV⟩⟩
refine ⟨V, H₁, ?_⟩
cases V
dsimp at H₂
subst H₂
exact hsV
· refine isTopologicalBasis_of_isOpen_of_nhds ?_ ?_
· rintro sU ⟨U, -, rfl⟩
exact U.2
· intro x sU hx hsU
rcases @h ⟨sU, hsU⟩ x hx with ⟨V, hV, H⟩
exact ⟨V, ⟨V, hV, rfl⟩, H⟩
