differentiable

Mathlib.Analysis.Calculus.FDeriv.Equiv

URI: https://scilib.ai/kg/mathlib#ContinuousLinearEquiv.differentiable

English

For iso: E ≃L[𝕜] F, iso is differentiable on s: DifferentiableOn 𝕜 iso s.

Русский

Для iso: E ≃L[𝕜] F, отображение iso дифференцируемо на множестве s: DifferentiableOn 𝕜 iso s.

LaTeX

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

Lean4

@[fun_prop]
protected theorem differentiable : Differentiable 𝕜 iso := fun _ => iso.differentiableAt

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

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

Разделы

Аффилиация

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