English
Let f : M → F₁ × F₂. Then ContMDiffOn I (I'.prod J') n f s is equivalent to ContMDiffOn I I' n (Prod.fst ∘ f) s and ContMDiffOn I J' n (Prod.snd ∘ f) s.
Русский
Пусть f : M → F₁ × F₂. Тогда ContMDiffOn(...) эквивалентно двум условиям для проекций.
LaTeX
$$$\\displaystyle \\operatorname{ContMDiffOn} \\\\ I \\\\ (I'.prod J') \\\\ n \\\\ f \\\\ s \\iff \\operatorname{ContMDiffOn} \\\\ I \\\\ I' \\\\ n \\\\ (\\mathrm{Prod.fst} \\circ f) \\\\ s \\land \\operatorname{ContMDiffOn} \\\\ I \\\\ J' \\\\ n \\\\ (\\mathrm{Prod.snd} \\circ f) \\\\ s$$
Lean4
/-- `ContMDiffWithinAt.comp₂`, with a separate argument for point equality. -/
theorem comp₂_of_eq {h : M' × N' → N} {f : M → M'} {g : M → N'} {x : M} {y : M' × N'} {t : Set (M' × N')}
(ha : ContMDiffWithinAt (I'.prod J') J n h t y) (fa : ContMDiffWithinAt I I' n f s x)
(ga : ContMDiffWithinAt I J' n g s x) (e : (f x, g x) = y) (st : MapsTo (fun x ↦ (f x, g x)) s t) :
ContMDiffWithinAt I J n (fun x ↦ h (f x, g x)) s x :=
by
rw [← e] at ha
exact ha.comp₂ fa ga st
