antilipschitz_equivRealProd — Mathlib

English

The map equivRealProd is antilipschitz with constant sqrt(2); i.e., ‖equivRealProd z1 − equivRealProd z2‖ ≥ c ‖z1 − z2‖ with c = sqrt(2) in NNReal.

Русский

Отображение equivRealProd антилипшицево с константой sqrt(2); то есть ∥equivRealProd z1 − equivRealProd z2∥ ≥ c ∥z1 − z2∥ с c = sqrt(2).

LaTeX

$$$ \\text{AntilipschitzWith } (\\mathbb{NNReal}.sqrt 2) (equivRealProd) $$$

Lean4

theorem antilipschitz_equivRealProd : AntilipschitzWith (NNReal.sqrt 2) equivRealProd :=
  AddMonoidHomClass.antilipschitz_of_bound equivRealProdLm fun z ↦ by
    simpa only [Real.coe_sqrt, NNReal.coe_ofNat] using norm_le_sqrt_two_mul_max z

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