ext_iff_nhds — Mathlib

English

Two topologies t and t' on X are equal iff their neighborhood filters at every point x coincide.

Русский

Две топологии t и t' на X равны тогда и только тогда, когда их окрестности в каждой точке x совпадают.

LaTeX

$$$t = t' \\iff \\forall x, \\ nhds^t(x) = nhds^{t'}(x)$$$

Lean4

theorem ext_iff_nhds {X} {t t' : TopologicalSpace X} : t = t' ↔ ∀ x, @nhds _ t x = @nhds _ t' x :=
  ⟨fun H _ ↦ congrFun (congrArg _ H) _, fun H ↦ by ext; simp_rw [@isOpen_iff_nhds _ _ _, H]⟩

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