lipschitzWith_im — Mathlib

English

The imaginary part map is 1-Lipschitz.

Русский

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

LaTeX

$$$$ lipschitzWith_im : LipschitzWith 1 (im (K := K)). $$$$

Lean4

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

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