contMDiffOn_infty — Mathlib

English

Relates ContMDiffWithinAt at nat level to At-level via equivalences.

Русский

Связь ContMDiffWithinAt на уровне nat с ContMDiffWithinAt в уровне At.

LaTeX

$$$ContMDiffWithinAt I I' n f s x \iff ∀ m: \mathbb{N}, (m : \mathbb{N}^\infty) \le n \Rightarrow ContMDiffWithinAt I I' m f s x$$$

Lean4

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

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