of_le — Mathlib

English

If a function is C^n at a point with respect to some order, then it is C^m at that point for any m ≤ n.

Русский

Если функция является $C^n$ в точке при некотором порядке, то она является $C^m$ в точке для любого $m \le n$.

LaTeX

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

Lean4

theorem of_le (hf : ContMDiffWithinAt I I' n f s x) (le : m ≤ n) : ContMDiffWithinAt I I' m f s x :=
  by
  simp only [ContMDiffWithinAt] at hf ⊢
  exact ⟨hf.1, hf.2.of_le (mod_cast le)⟩

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