contDiff_infty_iff_deriv — Mathlib

English

A standard equivalence: C^{n+1} ⇄ differentiable with derivative C^n.

Русский

Стандартное эквивалентное утверждение: C^{n+1} ⇄ дифференцируемость с производной C^n.

LaTeX

$$$contDiff\ 𝕜\ (n+1) f_2 \iff (Differentiable 𝕜 f_2) \land (ContDiff 𝕜 n (deriv f_2))$$$

Lean4

theorem contDiff_infty_iff_deriv : ContDiff 𝕜 ∞ f₂ ↔ Differentiable 𝕜 f₂ ∧ ContDiff 𝕜 ∞ (deriv f₂) :=
  by
  rw [show (∞ : WithTop ℕ∞) = ∞ + 1 from rfl, contDiff_succ_iff_deriv]
  simp

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