prodMap — Mathlib

English

Let f: M → M' × N' be differentiable on a set s and g: N → N' be differentiable on t. Then the product map (f,g) is differentiable on s × t.

Русский

Пусть f: M → M' × N' дифференцируемо на s, а g: N → N' дифференцируемо на t. Тогда Prod.map f g дифференцируемо на s × t.

LaTeX

$$$\text{MDifferentiableOn } I\,(I'.prod J')\ (\mathrm{Prod.map}\ f\ g)\ (s\timesˢ t) \iff \text{MDifferentiableOn } I I' f s ∧ \text{MDifferentiableOn } J J' g t$$

Lean4

theorem prodMap (hf : MDifferentiableOn I I' f s) (hg : MDifferentiableOn J J' g r) :
    MDifferentiableOn (I.prod J) (I'.prod J') (Prod.map f g) (s ×ˢ r) :=
  (hf.comp mdifferentiableOn_fst (prod_subset_preimage_fst _ _)).prodMk <|
    hg.comp mdifferentiableOn_snd (prod_subset_preimage_snd _ _)

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