not_inseparable_iff_exists_open — Mathlib

English

Not being inseparable is equivalent to the existence of an open set that separates the two points.

Русский

Неразделимость эквивалентна существованию открытого множества, которое отделяет две точки.

LaTeX

$$$\\\\neg (x \\\\sim_i y) \\\\iff \\\\exists s, IsOpen(s) \\\\wedge (x \\\\in s) \\\\oplus (y \\\\in s).$$$

Lean4

theorem not_inseparable_iff_exists_open : ¬(x ~ᵢ y) ↔ ∃ s : Set X, IsOpen s ∧ Xor' (x ∈ s) (y ∈ s) := by
  simp [inseparable_iff_forall_isOpen, ← xor_iff_not_iff]

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