of_le — Mathlib

English

If a function is C^n on a set, it remains C^m on the same set for any m ≤ n.

Русский

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

LaTeX

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

Lean4

theorem of_le (hf : ContMDiffOn I I' n f s) (le : m ≤ n) : ContMDiffOn I I' m f s := fun x hx => (hf x hx).of_le le

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