inseparable_iff_closure_eq — Mathlib

English

Two points are inseparable iff the closures of their singleton sets are equal.

Русский

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

LaTeX

$$$x \\sim_i y \\\\iff \\\\overline{\\{x\\}} = \\overline{\\{y\\}}.$$$

Lean4

theorem inseparable_iff_closure_eq : (x ~ᵢ y) ↔ closure ({ x } : Set X) = closure { y } := by
  simp only [inseparable_iff_specializes_and, specializes_iff_closure_subset, ← subset_antisymm_iff, eq_comm]

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