ext_iff — Mathlib

English

Two topologies on X are equal if and only if they have the same closed sets.

Русский

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

LaTeX

$$$t = g \iff \forall s, IsClosed[t] s \iff IsClosed[g] s$$$

Lean4

protected theorem ext_iff {t t' : TopologicalSpace X} : t = t' ↔ ∀ s, IsOpen[t] s ↔ IsOpen[t'] s :=
  ⟨fun h _ => h ▸ Iff.rfl, fun h => by ext; exact h _⟩

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