contMDiff_infty — Mathlib

English

Infinity-level ContMDiffOn is equivalent to holding for every finite n.

Русский

Континуальная гладкость на бесконечном уровне равна тому, что она выполняется для каждого конечного n.

LaTeX

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

Lean4

theorem contMDiff_infty : ContMDiff I I' ∞ f ↔ ∀ n : ℕ, ContMDiff I I' n f :=
  ⟨fun h _ => h.of_le (mod_cast le_top), fun h x => contMDiffWithinAt_infty.2 fun n => h n x⟩

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