lipschitz_apply — Mathlib

English

Every continuous linear map is Lipschitz with Lipschitz constant equal to its NN-norm.

Русский

Каждое непрерывно линейное отображение липшицево с константой равной nnnorm самого отображения.

LaTeX

$$LipschitzWith (nnnorm f) f$$

Lean4

/-- Evaluation of a continuous linear map `f` at a point is Lipschitz continuous in `f`. -/
theorem lipschitz_apply (x : E) : LipschitzWith ‖x‖₊ fun f : E →SL[σ₁₂] F => f x :=
  lipschitzWith_iff_norm_sub_le.2 fun f g => ((f - g).le_opNorm x).trans_eq (mul_comm _ _)

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