English
The first coordinate projection remains C^n after restricting to a subset.
Русский
Первая координата сохраняет гладкость при ограничении.
LaTeX
$$contMDiffWithinAt_fst {s : Set (M × N)} {p : M × N} : ContMDiffWithinAt (I.prod J) I n Prod.fst s p$$
Lean4
theorem contMDiffWithinAt_snd {s : Set (M × N)} {p : M × N} : ContMDiffWithinAt (I.prod J) J n Prod.snd s p := by
/- porting note: `simp` fails to apply lemmas to `ModelProd`. Was
rw [contMDiffWithinAt_iff']
refine' ⟨continuousWithinAt_snd, _⟩
refine' contDiffWithinAt_snd.congr (fun y hy => _) _
· simp only [mfld_simps] at hy
simp only [hy, mfld_simps]
· simp only [mfld_simps]
-/
rw [contMDiffWithinAt_iff']
refine ⟨continuousWithinAt_snd, contDiffWithinAt_snd.congr (fun y hy => ?_) ?_⟩
· exact (extChartAt J p.2).right_inv ⟨hy.1.1.2, hy.1.2.2⟩
· exact (extChartAt J p.2).right_inv <| (extChartAt J p.2).map_source (mem_extChartAt_source _)
