inseparable_iff_forall_isClosed — Mathlib

English

Two points are inseparable iff for every closed set, membership of the two points coincides.

Русский

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

LaTeX

$$$x \\sim_i y \\iff \\forall C, C \\text{ closed} \\Rightarrow (x \\in C \\iff y \\in C).$$$

Lean4

theorem inseparable_iff_forall_isClosed : (x ~ᵢ y) ↔ ∀ s : Set X, IsClosed s → (x ∈ s ↔ y ∈ s) := by
  simp only [inseparable_iff_specializes_and, specializes_iff_forall_closed, ← forall_and, ← iff_def]

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