ext_iff_isClosed — Mathlib

English

Two topologies are equal iff they have the same closed sets.

Русский

Две топологии равны, если у них совпадают замкнутые множества.

LaTeX

$$$t_1 = t_2 \iff \forall s, IsClosed[t_1] s \iff IsClosed[t_2] s$$$

Lean4

theorem ext_iff_isClosed {X} {t₁ t₂ : TopologicalSpace X} : t₁ = t₂ ↔ ∀ s, IsClosed[t₁] s ↔ IsClosed[t₂] s :=
  by
  rw [TopologicalSpace.ext_iff, compl_surjective.forall]
  simp only [@isOpen_compl_iff _ _ t₁, @isOpen_compl_iff _ _ t₂]

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