lipschitzWith_re — Mathlib

English

The real part map is 1-Lipschitz.

Русский

Функция вещественной части линейно-ограничена Липшицем 1.

LaTeX

$$$$ lipschitzWith_re : LipschitzWith 1 (re (K := K)). $$$$

Lean4

theorem lipschitzWith_re : LipschitzWith 1 (re (K := K)) :=
  by
  intro x y
  simp only [ENNReal.coe_one, one_mul, edist_eq_enorm_sub]
  calc
    ‖re x - re y‖ₑ
    _ = ‖re (x - y)‖ₑ := by rw [AddMonoidHom.map_sub re x y]
    _ ≤ ‖x - y‖ₑ := by rw [enorm_le_iff_norm_le]; exact norm_re_le_norm (x - y)

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