hasFDerivAt_prodMk_right — Mathlib

English

The map f0 ↦ (e0, f0) from F to E × F is differentiable at f0 with derivative the right injection h ↦ (0, h).

Русский

Отображение f0 ↦ (e0, f0) из пространства F в произведение E × F дифференцируемо в точке f0, производная равна линейному отображению h ↦ (0, h).

LaTeX

$$$\text{HasFDerivAt}\big(\lambda f:F, (e_0,f)\big)$\text{inr } 𝕜 E F$ f_0$$$

Lean4

@[fun_prop]
theorem hasFDerivAt_prodMk_right (e₀ : E) (f₀ : F) : HasFDerivAt (fun f : F => (e₀, f)) (inr 𝕜 E F) f₀ :=
  (hasFDerivAt_const e₀ f₀).prodMk (hasFDerivAt_id f₀)

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