inseparable_iff_mem_closure — Mathlib

English

Two points are inseparable iff each lies in the closure of the singleton of the other.

Русский

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

LaTeX

$$$x \\sim_i y \\\\iff x \\in \\overline{\\{y\\}} \\\\wedge y \\in \\overline{\\{x\\}}.$$$

Lean4

theorem inseparable_iff_mem_closure : (x ~ᵢ y) ↔ x ∈ closure ({ y } : Set X) ∧ y ∈ closure ({ x } : Set X) :=
  inseparable_iff_specializes_and.trans <| by simp only [specializes_iff_mem_closure, and_comm]

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