mdifferentiableAt — Mathlib

English

For every x in M, the derivative of e at x exists in the MDifferentiable sense: MDifferentiableAt I I' e x.

Русский

Для каждого x в M существует производная отображения e в точке x в смысле MDifferentiableAt: I → I' на e x.

LaTeX

$$$\mathrm{MDifferentiableAt}(I,I',e,x)$$$

Lean4

protected theorem mdifferentiableAt {x : M} (hx : x ∈ e.source) : MDifferentiableAt I I' e x :=
  (he.1 x hx).mdifferentiableAt (e.open_source.mem_nhds hx)

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