inseparable_iff_forall_isOpen — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem inseparable_iff_forall_isOpen : (x ~ᵢ y) ↔ ∀ s : Set X, IsOpen s → (x ∈ s ↔ y ∈ s) := by
  simp only [inseparable_iff_specializes_and, specializes_iff_forall_open, ← forall_and, ← iff_def, Iff.comm]

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