mono

Mathlib.Analysis.Calculus.FDeriv.Basic

URI: https://scilib.ai/kg/mathlib#DifferentiableOn.mono

English

If f is differentiable on t and s ⊆ t, then f is differentiable on s.

Русский

Если f дифференцируема на t, и s ⊆ t, то дифференцируема на s.

LaTeX

$$$\text{DifferentiableOn } 𝕜 f t \land s \subset t \Rightarrow \text{DifferentiableOn } 𝕜 f s$$$

Lean4

theorem mono (h : DifferentiableOn 𝕜 f t) (st : s ⊆ t) : DifferentiableOn 𝕜 f s := fun x hx => (h x (st hx)).mono st

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

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

Разделы

Аффилиация

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