contDiffOn_iff_forall_nat_le

Mathlib.Analysis.Calculus.ContDiff.Defs

URI: https://scilib.ai/kg/mathlib#contDiffOn_iff_forall_nat_le

← MathLib Explorer

English

If ContDiffOn 𝕜 (n+1) f s, then ContDiffOn 𝕜 1 f s.

Русский

Если ContDiffOn 𝕜 (n+1) f s, то ContDiffOn 𝕜 1 f s.

LaTeX

$$$\forall f,s: ContDiffOn 𝕜 (n+1) f s \Rightarrow ContDiffOn 𝕜 1 f s.$$

Lean4

theorem contDiffOn_iff_forall_nat_le {n : ℕ∞} : ContDiffOn 𝕜 n f s ↔ ∀ m : ℕ, ↑m ≤ n → ContDiffOn 𝕜 m f s :=
  ⟨fun H _ hm => H.of_le (mod_cast hm), fun H x hx m hm => H m hm x hx m le_rfl⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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