lipschitz — Mathlib

English

If f approximates a linear map on s with constant c, then f restricted to s is a continuous function.

Русский

Если f аппроксимирует линейное отображение на s с константой c, то ограничение f на s непрерывно.

LaTeX

$$hf : ApproximatesLinearOn f f' s c → Continuous (s.restrict f)$$

Lean4

protected theorem lipschitz (hf : ApproximatesLinearOn f f' s c) : LipschitzWith (‖f'‖₊ + c) (s.restrict f) := by
  simpa only [restrict_apply, add_sub_cancel] using (f'.lipschitz.restrict s).add hf.lipschitz_sub

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