mdifferentiableWithinAt — Mathlib

English

A continuous linear map f is differentiable in the MF-sense within any set.

Русский

Пусть f — непрерывно линейное отображение; оно дифференцируемо в смысле MF внутри любого множества.

LaTeX

$$MDifferentiableWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') f s x$$

Lean4

protected theorem mdifferentiableWithinAt : MDifferentiableWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') f s x :=
  f.differentiableWithinAt.mdifferentiableWithinAt

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