contDiffOn_infty_iff_deriv_of_isOpen

English

The statement for ∞ follows from succ case; Infinity case is equivalent to differentiability and derivative ∞-smoothness.

Русский

Предпосылка бесконечности следует из случаяsucc; бесконечная гладкость сводится к дифференцируемости и бесконечно-гладкой производной.

LaTeX

$$$contDiffOn\ 𝕜\ ∞ f_2\ s_2 \iff DifferentiableOn 𝕜 f_2\ s_2 \land ContDiffOn 𝕜 \∞ (derivWithin f_2 \ s_2) \ s_2$$$

Lean4

theorem contDiffOn_infty_iff_deriv_of_isOpen (hs : IsOpen s₂) :
    ContDiffOn 𝕜 ∞ f₂ s₂ ↔ DifferentiableOn 𝕜 f₂ s₂ ∧ ContDiffOn 𝕜 ∞ (deriv f₂) s₂ :=
  by
  rw [show ∞ = ∞ + 1 by rfl, contDiffOn_succ_iff_deriv_of_isOpen hs]
  simp

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