English
A set s belongs to the neighborhood filter of a point a iff there exists a basis element b containing a with b ⊆ s.
Русский
Множество s принадлежит окрестной фильтр а точке a тогда и только тогда, когда существует элемент базиса b с a ∈ b ⊆ s.
LaTeX
$$mem_nhds_iff {a : α} {s : Set α} {b : Set (Set α)} (hb : IsTopologicalBasis b) : s ∈ 𝓝 a ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s$$
Lean4
/-- A set `s` is in the neighbourhood of `a` iff there is some basis set `t`, which
contains `a` and is itself contained in `s`. -/
theorem mem_nhds_iff {a : α} {s : Set α} {b : Set (Set α)} (hb : IsTopologicalBasis b) :
s ∈ 𝓝 a ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s :=
by
change s ∈ (𝓝 a).sets ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s
rw [hb.eq_generateFrom, nhds_generateFrom, biInf_sets_eq]
· simp [and_assoc, and_left_comm]
· rintro s ⟨hs₁, hs₂⟩ t ⟨ht₁, ht₂⟩
let ⟨u, hu₁, hu₂, hu₃⟩ := hb.1 _ hs₂ _ ht₂ _ ⟨hs₁, ht₁⟩
exact
⟨u, ⟨hu₂, hu₁⟩, le_principal_iff.2 (hu₃.trans inter_subset_left),
le_principal_iff.2 (hu₃.trans inter_subset_right)⟩
· rcases eq_univ_iff_forall.1 hb.sUnion_eq a with ⟨i, h1, h2⟩
exact ⟨i, h2, h1⟩
