inseparable_iff — Mathlib

English

In a pseudometric space, two points x and y are inseparable if and only if their distance dist x y is zero.

Русский

В псевдометрическом пространстве две точки x и y неразделимы тогда и только тогда, когда расстояние между ними dist(x,y) равно нулю.

LaTeX

$$$\\mathrm{Inseparable}(x,y) \\iff \\operatorname{dist}(x,y)=0$$$

Lean4

theorem inseparable_iff {x y : α} : Inseparable x y ↔ dist x y = 0 := by
  rw [Metric.inseparable_iff_nndist, dist_nndist, NNReal.coe_eq_zero]

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