of_le — Mathlib

English

If ContMDiffAt holds for order n at a point, then it also holds for any smaller order m ≤ n at that point.

Русский

Если ContMDiffAt верно для порядка n в точке, то оно верно и для любого меньшего порядка m ≤ n в той же точке.

LaTeX

$$ContMDiffAt\, I\, I'\, n\, f\, x \rightarrow WithTop\, le\, m\;\Rightarrow\; ContMDiffAt\, I\, I'\, m\, f\, x$$

Lean4

theorem of_le (hf : ContMDiffAt I I' n f x) (le : m ≤ n) : ContMDiffAt I I' m f x :=
  ContMDiffWithinAt.of_le hf le

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