ext — Mathlib

English

Two topologies on the same set are equal if and only if they have the same open sets.

Русский

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

LaTeX

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

Lean4

@[ext (iff := false)]
protected theorem ext : ∀ {f g : TopologicalSpace X}, IsOpen[f] = IsOpen[g] → f = g
  | ⟨_, _, _, _⟩, ⟨_, _, _, _⟩, rfl => rfl

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