English
If ContDiffWithinAt 𝕜 n f s x holds, then reducing the index to any m ≤ n preserves the same property: ContDiffWithinAt 𝕜 m f s x.
Русский
Если ContDiffWithinAt 𝕜 n f s x верна, то для любого m ≤ n верна тоже ContDiffWithinAt 𝕜 m f s x.
LaTeX
$$$ ContDiffWithinAt 𝕜 n f s x \\Rightarrow \\forall m \\le n,\\ ContDiffWithinAt 𝕜 m f s x \\quad\\text{and conversely }\\ ContDiffWithinAt 𝕜 n f s x \\Leftarrow \\ for\\le Top. $$
Lean4
@[fun_prop]
theorem of_le (h : ContDiffWithinAt 𝕜 n f s x) (hmn : m ≤ n) : ContDiffWithinAt 𝕜 m f s x := by
match n with
| ω =>
match m with
| ω => exact h
| (m : ℕ∞) =>
intro k _
obtain ⟨u, hu, p, hp, -⟩ := h
exact ⟨u, hu, p, hp.of_le le_top⟩
| (n : ℕ∞) =>
match m with
| ω => simp at hmn
| (m : ℕ∞) => exact fun k hk ↦ h k (le_trans hk (mod_cast hmn))
