mdifferentiableAt — Mathlib

English

Let f be differentiable on a set s with respect to the structures I and I'. If s is a neighborhood of x (i.e., s contains a neighborhood of x), then f is differentiable at x (in the sense of I and I').

Русский

Пусть f дифференцируема на множестве s относительно структур I и I'. Если s содержит окрестность x (то есть s является окрестностью x), то f дифференцируема в точке x (с учётом I и I').

LaTeX

$$$MDifferentiableOn\, I\, I'\, f\, s \wedge s \in \\mathcal{N}(x) \\Rightarrow MDifferentiableAt\, I\, I'\, f\, x$$$

Lean4

theorem mdifferentiableAt (h : MDifferentiableOn I I' f s) (hx : s ∈ 𝓝 x) : MDifferentiableAt I I' f x :=
  (h x (mem_of_mem_nhds hx)).mdifferentiableAt hx

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