nhds_nhdsAdjoint_of_ne — Mathlib

English

If b ≠ a, then nhds in nhdsAdjoint(a,f) at b is pure b.

Русский

Если b ≠ a, то окрестностной фильтр в nhdsAdjoint(a,f) на b равен чистому фильтру b.

LaTeX

$$theorem nhds_nhdsAdjoint_of_ne {a b : α} (f : Filter α) (h : b ≠ a) : @nhds α (nhdsAdjoint a f) b = pure b$$

Lean4

theorem nhds_nhdsAdjoint_of_ne {a b : α} (f : Filter α) (h : b ≠ a) : @nhds α (nhdsAdjoint a f) b = pure b :=
  let _ := nhdsAdjoint a f
  (isOpen_singleton_iff_nhds_eq_pure _).1 <| isOpen_singleton_nhdsAdjoint f h

Похожие утверждения