English
Variant of the WithinAt lemma for product maps: if hf and hg are differentiable within at at p.1 and p.2, then the product map is differentiable within at at p.
Русский
Вариант леммы WithinAt для произведения: если hf и hg дифференцируемы внутри на p.1 и p.2, то произведение дифференцируемо внутри на p.
LaTeX
$$$\forall p=(p_1,p_2)\in 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 tangentMapWithin_prodSnd {s : Set (M × M')} {p : TangentBundle (I.prod I') (M × M')}
(hs : UniqueMDiffWithinAt (I.prod I') s p.proj) :
tangentMapWithin (I.prod I') I' Prod.snd s p = ⟨p.proj.2, p.2.2⟩ :=
by
simp only [tangentMapWithin]
rw [mfderivWithin_snd]
· rcases p with ⟨⟩; rfl
· exact hs
