contDiff_infty

Mathlib.Analysis.Calculus.ContDiff.Defs

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

English

ContDiffOn on universal set is equivalent to ContDiff.

Русский

ContDiffOn на всём множестве эквивалентно ContDiff.

LaTeX

$$$contDiffOn_univ : ContDiffOn 𝕜 n f Set.univ\leftrightarrow ContDiff 𝕜 n f$$$

Lean4

theorem contDiff_infty : ContDiff 𝕜 ∞ f ↔ ∀ n : ℕ, ContDiff 𝕜 n f := by simp [contDiffOn_univ.symm, contDiffOn_infty]

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

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

Разделы

Аффилиация

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