iteratedFDeriv_clm_apply_const_apply

English

The inverse (E × (F × G)) ≃ ((E × F) × G) is smooth.

Русский

Обратное отображение (E × (F × G)) ≃ ((E × F) × G) гладко отображается.

LaTeX

$$$\operatorname{ContDiff}_{\mathbb{K}} n ((\mathrm{prodAssoc}\; E\; F\; G)^{-1})$$$

Lean4

/-- Application of a `ContinuousLinearMap` to a constant commutes with `iteratedFDeriv`. -/
theorem iteratedFDeriv_clm_apply_const_apply {c : E → F →L[𝕜] G} (hc : ContDiff 𝕜 n c) {i : ℕ} (hi : i ≤ n) {x : E}
    {u : F} {m : Fin i → E} : (iteratedFDeriv 𝕜 i (fun y ↦ (c y) u) x) m = (iteratedFDeriv 𝕜 i c x) m u :=
  by
  simp only [← iteratedFDerivWithin_univ]
  exact iteratedFDerivWithin_clm_apply_const_apply uniqueDiffOn_univ hc.contDiffOn hi (mem_univ _)

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