English
A function approximates a linear map f' on a set s with constant c if for any x,y ∈ s the deviation from linearity is bounded by c times the distance between x and y.
Русский
Функция аппроксимирует линейное отображение f' на множестве s с константой c, если для любых x,y ∈ s отклонение от линейности ограничено c на расстояние между x и y.
LaTeX
$$$\forall x,y \in s, \|f x - f y - f'(x-y)\| ≤ c \|x-y\|$$$
Lean4
/-- We say that `f` approximates a continuous linear map `f'` on `s` with constant `c`,
if `‖f x - f y - f' (x - y)‖ ≤ c * ‖x - y‖` whenever `x, y ∈ s`.
This predicate is defined to facilitate the splitting of the inverse function theorem into small
lemmas. Some of these lemmas can be useful, e.g., to prove that the inverse function is defined
on a specific set. -/
def ApproximatesLinearOn (f : E → F) (f' : E →L[𝕜] F) (s : Set E) (c : ℝ≥0) : Prop :=
∀ x ∈ s, ∀ y ∈ s, ‖f x - f y - f' (x - y)‖ ≤ c * ‖x - y‖
