eq_iff — Mathlib

English

In a T0 space with basis b, x=y iff for all s in b, x∈s ⇔ y∈s.

Русский

В T0-пространстве с базисом b, x=y тогда и только тогда, когда для всех s∈b выполняется x∈s ⇔ y∈s.

LaTeX

$$$x=y \iff ∀ s\in b, x\in s \leftrightarrow y\in s$.$$

Lean4

theorem eq_iff [T0Space X] {b : Set (Set X)} (hb : IsTopologicalBasis b) {x y : X} : x = y ↔ ∀ s ∈ b, (x ∈ s ↔ y ∈ s) :=
  inseparable_iff_eq.symm.trans hb.inseparable_iff

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