lipschitzWith_toNNReal — Mathlib

English

The real-to-NNReal map is 1-Lipschitz.

Русский

Переход из действительных чисел в NNReal по модулю нормированной меры — 1-липшицев.

LaTeX

$$$\\operatorname{LipschitzWith}(1,\\, \\operatorname{Real.toNNReal})$$$

Lean4

theorem _root_.Real.lipschitzWith_toNNReal : LipschitzWith 1 Real.toNNReal :=
  by
  refine lipschitzWith_iff_dist_le_mul.mpr (fun x y ↦ ?_)
  simpa only [NNReal.coe_one, dist_prod_same_right, one_mul, Real.dist_eq] using
    lipschitzWith_iff_dist_le_mul.mp lipschitzWith_max (x, 0) (y, 0)

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