lipschitz_equivRealProd — Mathlib

English

The map equivRealProd is 1-Lipschitz, i.e., ‖equivRealProd(z1) − equivRealProd(z2)‖ ≤ ‖z1 − z2‖ for all z1,z2 ∈ ℂ.

Русский

Отображение equivRealProd является 1-Lipschitz: для любых z1,z2 ∈ ℂ выполняется неравенство нормы разности: \\|equivRealProd(z1) − equivRealProd(z2)\\| ≤ \\|z1 − z2\\|.

LaTeX

$$$ \\text{LipschitzWith } 1 \\; (\\text{equivRealProd}) $$$

Lean4

theorem lipschitz_equivRealProd : LipschitzWith 1 equivRealProd := by
  simpa using AddMonoidHomClass.lipschitz_of_bound equivRealProdLm 1 equivRealProd_apply_le'

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