inseparable_iff_nndist — Mathlib

English

In a pseudometric space, two points x and y are inseparable if and only if their nonnegative distance nndist x y is equal to 0.

Русский

В псевдометрическом пространстве две точки x и y неразделимы тогда и только тогда, когда их неотрицательное расстояние nndist(x, y) равно 0.

LaTeX

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

Lean4

theorem inseparable_iff_nndist {x y : α} : Inseparable x y ↔ nndist x y = 0 := by
  rw [EMetric.inseparable_iff, edist_nndist, ENNReal.coe_eq_zero]

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