inseparable_eq_eq — Mathlib

English

For a T0 space with a basis b, inseparability of x and y is equivalent to membership agreement across all basis sets.

Русский

Для T0-пространства с базисом b неразделимость x и y эквивалентна согласованности принадлежности по всем элементам базиса.

LaTeX

$$$Inseparable(x,y) \iff \forall s\in b, (x\in s \leftrightarrow y\in s).$$$

Lean4

@[simp]
theorem inseparable_eq_eq [T0Space X] : Inseparable = @Eq X :=
  funext₂ fun _ _ => propext inseparable_iff_eq

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