isBoundedSMul — Mathlib

English

The real numbers carry a Lipschitz-add structure, i.e., addition is Lipschitz with constant 2.

Русский

У действительных чисел есть структура LipschitzAdd: сложение — липшицево ограничено константой 2.

LaTeX

$$LipschitzAdd \\mathbb{R}$$

Lean4

instance isBoundedSMul : IsBoundedSMul ℝ ℝ
    where
  dist_smul_pair' x y₁ y₂ := by simpa [Real.dist_eq, mul_sub] using (abs_mul x (y₁ - y₂)).le
  dist_pair_smul' x₁ x₂ y := by simpa [Real.dist_eq, sub_mul] using (abs_mul (x₁ - x₂) y).le

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