tangentMap_prod_left — Mathlib

English

Variant asserting existence of product map differentiability at a point p in the product space when each component is differentiable at its projection points.

Русский

Вариант утверждает существование дифференцируемости произведения в точке p для компонент, дифференцируемых на проекциях.

LaTeX

$$$\forall p: M×N, hf:MDifferentiableWithinAt I I' f s p.1, hg:MDifferentiableWithinAt J J' g r p.2 \Rightarrow MDifferentiableWithinAt (I.prod J) (I'.prod J') (Prod.map f g) (s ×ˢ r) p$$$

Lean4

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

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