edist_lt_top — Mathlib

English

If f is an AntilipschitzWith map, then the edistance between any two points is finite.

Русский

Если отображение антип Lipschitz, тогда расстояние ed между любыми двумя точками конечно.

LaTeX

$$$edist(x,y) < \\top$$$

Lean4

protected theorem edist_lt_top [PseudoEMetricSpace α] [PseudoMetricSpace β] {K : ℝ≥0} {f : α → β}
    (h : AntilipschitzWith K f) (x y : α) : edist x y < ⊤ :=
  (h x y).trans_lt <| ENNReal.mul_lt_top ENNReal.coe_lt_top (edist_lt_top _ _)

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