of_le

Mathlib.Analysis.Calculus.ContDiff.Defs

URI: https://scilib.ai/kg/mathlib#ContDiffAt.of_le

English

If ContDiffAt holds at level n, then it holds at any lower level m ≤ n.

Русский

Если ContDiffAt выполнено на уровне n, то оно выполняется и на любом более низком уровне m ≤ n.

LaTeX

$$$\\forall m \\le n, \\ContDiffAt 𝕜 n f x \\Rightarrow \\ContDiffAt 𝕜 m f x$$$

Lean4

theorem of_le (h : ContDiffAt 𝕜 n f x) (hmn : m ≤ n) : ContDiffAt 𝕜 m f x :=
  ContDiffWithinAt.of_le h hmn

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

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

Разделы

Аффилиация

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