contMDiffWithinAt_iff_nat — Mathlib

English

Equates nat-level ContMDiffOn with ENat treatment via cast.

Русский

Эквивалентность ContMDiffOn на уровне натурального с ENat посредством приведения.

LaTeX

$$$contMDiffOn_infty : ContMDiffOn I I' ∞ f s \iff ∀ n: \mathbb{N}, ContMDiffOn I I' n f s$$$

Lean4

theorem contMDiffWithinAt_iff_nat {n : ℕ∞} :
    ContMDiffWithinAt I I' n f s x ↔ ∀ m : ℕ, (m : ℕ∞) ≤ n → ContMDiffWithinAt I I' m f s x :=
  by
  refine ⟨fun h m hm => h.of_le (mod_cast hm), fun h => ?_⟩
  obtain - | n := n
  · exact contMDiffWithinAt_infty.2 fun n => h n le_top
  · exact h n le_rfl

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