contMDiffWithinAt_infty — Mathlib

English

Infinite ENat case reduces to nat version for all n.

Русский

Бесконечный ENat-порядок сводится к Натуральному для всех n.

LaTeX

$$$contMDiff_infty : ContMDiff I I' ∞ f \iff ∀ n: \mathbb{N}, ContMDiff I I' n f$$$

Lean4

theorem contMDiffWithinAt_infty : ContMDiffWithinAt I I' ∞ f s x ↔ ∀ n : ℕ, ContMDiffWithinAt I I' n f s x :=
  ⟨fun h n => ⟨h.1, contDiffWithinAt_infty.1 h.2 n⟩, fun H => ⟨(H 0).1, contDiffWithinAt_infty.2 fun n => (H n).2⟩⟩

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