differentiableOn

Mathlib.Analysis.Calculus.Deriv.AffineMap

URI: https://scilib.ai/kg/mathlib#AffineMap.differentiableOn

English

For an affine map f, f is differentiable on any set s; i.e., DifferentiableOn 𝕜 f s.

Русский

Для аффинного отображения f дифференцируемо на любом множестве s; то есть DifferentiableOn 𝕜 f s.

LaTeX

$$$\\text{DifferentiableOn}_{𝕜}(f,s).$$$

Lean4

protected theorem differentiableOn : DifferentiableOn 𝕜 f s := fun _ _ ↦ f.differentiableWithinAt

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru