English
The set A(f, L, r, ε) consists of points x around which the function f is well approximated by the linear map L at scale r with error ε.
Русский
Множество A(f, L, r, ε) состоит из точек x, вокруг которых функция f хорошо аппроксимируется линейным отображением L на масштабе r с погрешностью ε.
LaTeX
$$$$A(f,L,r,\varepsilon) = \{ x \in E \mid \exists r' \in Ioc(r/2,r), \; \forall y,z \in B(x,r'), \; \|f(z)-f(y)-L(z-y)\| < \varepsilon \cdot r \}.$$$$
Lean4
/-- The set `A f L r ε` is the set of points `x` around which the function `f` is well approximated
at scale `r` by the linear map `L`, up to an error `ε`. We tweak the definition to make sure that
this is an open set. -/
def A (f : E → F) (L : E →L[𝕜] F) (r ε : ℝ) : Set E :=
{x | ∃ r' ∈ Ioc (r / 2) r, ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖f z - f y - L (z - y)‖ < ε * r}
