hasFDerivAt_prodMk_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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