English
For any n: α → Filter α and a ∈ α with HasBasis structure, nhds in the mkOfNhds topology equals n a, under suitable basis/hasBasis conditions.
Русский
Для любого n: α → Filter α и точки a, если заданы условия HasBasis, тогда окрестности в mkOfNhds равны n a при подходящих условиях.
LaTeX
$$$\\text{nhds}(a) = n(a).$$$
Lean4
theorem nhds_mkOfNhds_single [DecidableEq α] {a₀ : α} {l : Filter α} (h : pure a₀ ≤ l) (b : α) :
@nhds α (TopologicalSpace.mkOfNhds (update pure a₀ l)) b = (update pure a₀ l : α → Filter α) b :=
by
refine nhds_mkOfNhds _ _ (le_update_iff.mpr ⟨h, fun _ _ => le_rfl⟩) fun a s hs => ?_
rcases eq_or_ne a a₀ with (rfl | ha)
· filter_upwards [hs] with b hb
rcases eq_or_ne b a with (rfl | hb)
· exact hs
· rwa [update_of_ne hb]
· simpa only [update_of_ne ha, mem_pure, eventually_pure] using hs
