English
If hf and hg are ContMDiffAt, then the product map is ContMDiffAt with product structure.
Русский
Если hf и hg — ContMDiffAt, то произведение гладко.
LaTeX
$$ContMDiffAt I (I'.prod J') n (λ x, (f x, g x)) x$$
Lean4
theorem contMDiffWithinAt_fst {s : Set (M × N)} {p : M × N} : ContMDiffWithinAt (I.prod J) I n Prod.fst s p := by
/- porting note: `simp` fails to apply lemmas to `ModelProd`. Was
rw [contMDiffWithinAt_iff']
refine' ⟨continuousWithinAt_fst, _⟩
refine' contDiffWithinAt_fst.congr (fun y hy => _) _
· simp only [mfld_simps] at hy
simp only [hy, mfld_simps]
· simp only [mfld_simps]
-/
rw [contMDiffWithinAt_iff']
refine ⟨continuousWithinAt_fst, contDiffWithinAt_fst.congr (fun y hy => ?_) ?_⟩
· exact (extChartAt I p.1).right_inv ⟨hy.1.1.1, hy.1.2.1⟩
· exact (extChartAt I p.1).right_inv <| (extChartAt I p.1).map_source (mem_extChartAt_source _)
