tangentMap_prod_right — Mathlib

English

If f and g are MDifferentiableAt at x and y, then Prod.map f g is MDifferentiableAt at (x,y).

Русский

Если f и g дифференцируемы в точках x и y, то произведение дифференцируемо в точке (x,y).

LaTeX

$$$\text{MDifferentiableAt } I I' f x \land \text{MDifferentiableAt } J J' g y \Rightarrow \text{MDifferentiableAt } (I.prod J) (I'.prod J') (\mathrm{Prod.map} f g) (x,y)$$$

Lean4

theorem tangentMap_prod_right {p : TangentBundle I' M'} {x₀ : M} :
    tangentMap I' (I.prod I') (fun y => (x₀, y)) p = ⟨(x₀, p.1), (0, p.2)⟩ :=
  by
  simp only [tangentMap, mfderiv_prod_right, TotalSpace.mk_inj]
  rfl

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