contDiff_all_iff_nat — Mathlib

English

The ContDiff_all theorem states equivalence between ContDiff at ENat levels and Nat levels.

Русский

Теорема ContDiffAll утверждает эквивалентность между ContDiff на уровнях ENat и Nat.

LaTeX

$$$ContDiffAll\ 𝕜\ f\equiv (\forall n: ENat, ContDiff 𝕜 (WithTop.some n) f)\iff (\forall n: Nat, ContDiff 𝕜 (n.cast) f)$$$

Lean4

theorem contDiff_all_iff_nat : (∀ n : ℕ∞, ContDiff 𝕜 n f) ↔ ∀ n : ℕ, ContDiff 𝕜 n f := by
  simp only [← contDiffOn_univ, contDiffOn_all_iff_nat]

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