inseparable_iff — Mathlib

English

In a pseudo-EMetric space, two points x and y are inseparable if and only if edist x y = 0.

Русский

В псевдо-эметрическом пространстве две точки x и y неразделимы тогда и только тогда, когда их edist равен нулю.

LaTeX

$$$Inseparable x y \iff edist x y = 0$$$

Lean4

theorem inseparable_iff : Inseparable x y ↔ edist x y = 0 := by
  simp [inseparable_iff_mem_closure, mem_closure_iff, edist_comm, forall_gt_iff_le]

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