lipschitzWith_sup_right — Mathlib

English

For every z in α, the map x ↦ x ⊔ z is 1-Lipschitz with respect to the norm, i.e., ‖(x ⊔ z) − (y ⊔ z)‖ ≤ ‖x − y‖ for all x, y.

Русский

Для любого z в α отображение x ↦ x ⊔ z является 1‑липшицевым по норме: для всех x, y выполняется ‖(x ⊔ z) − (y ⊔ z)‖ ≤ ‖x − y‖.

LaTeX

$$$\|x \lor z - (y \lor z)\| \le \|x - y\|$$$

Lean4

theorem lipschitzWith_sup_right (z : α) : LipschitzWith 1 fun x => x ⊔ z :=
  LipschitzWith.of_dist_le_mul fun x y =>
    by
    rw [NNReal.coe_one, one_mul, dist_eq_norm, dist_eq_norm]
    exact norm_sup_sub_sup_le_norm x y z

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