English
For a map f: M → M' × N', differentiability within a set s is equivalent to differentiability of its coordinate compositions: MDifferentiableWithinAt I (I'.prod J') f s x iff MDifferentiableWithinAt I I' (Prod.fst ∘ f) s x and MDifferentiableWithinAt I J' (Prod.snd ∘ f) s x.
Русский
Для отображения f: M → M' × N' дифференцируемость внутри множества s эквивалентна дифференцируемости его координатных композиции.
LaTeX
$$$\mathrm{MDifferentiableWithinAt}\, I\, (I'.prod J')\, f\, s\, x \iff \left(\mathrm{MDifferentiableWithinAt}\, I\, I'\, (\mathrm{Prod.fst} \circ f)\, s\, x \land \mathrm{MDifferentiableWithinAt}\, I\, J'\, (\mathrm{Prod.snd} \circ f)\, s\, x\right)$$$
Lean4
theorem mdifferentiableOn_snd {s : Set (M × M')} : MDifferentiableOn (I.prod I') I' Prod.snd s :=
mdifferentiable_snd.mdifferentiableOn
