continuous — Mathlib

English

If a function f is approximated by a continuous linear map f' on a set s with constant c, then f is continuous on s.

Русский

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

LaTeX

$$$\text{ApproximatesLinearOn}(f, f', s, c) \implies \text{Continuous}(f|_s).$$

Lean4

protected theorem continuous (hf : ApproximatesLinearOn f f' s c) : Continuous (s.restrict f) :=
  hf.lipschitz.continuous

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