English
Let φ: E → F0 and φs: E → ∀ i, F'(Fin.succ i). Then the map x ↦ Fin.cons(φ(x)) (φs(x)) is differentiable with respect to 𝕜 if and only if φ is differentiable and φs is differentiable with respect to 𝕜. In other words, a map into a finite product is differentiable exactly when each coordinate map is differentiable.
Русский
Пусть φ: E → F0 и φs: E → ∀ i, F'(Fin.succ i). Тогда отображение x ↦ Fin.cons(φ(x)) (φs(x)) дифференцируемо по 𝕜 тогда и только если φ дифференцируемо по 𝕜 и φs дифференцируемо по 𝕜. Другими словами, отображение в конечный произведение дифференцируемо тогда и только тогда, когда каждая координата дифференцируема.
LaTeX
$$$ \operatorname{Differentiable}_{\mathbb{k}}\left(\lambda x:\,E\;\mapsto\; \mathrm{Fin.cons}(\phi x)(\phi_s x)\right) \;\iff\; \operatorname{Differentiable}_{\mathbb{k}}(\phi) \wedge \operatorname{Differentiable}_{\mathbb{k}}(\phi_s). $$$
Lean4
theorem differentiable_finCons :
Differentiable 𝕜 (fun x => Fin.cons (φ x) (φs x)) ↔ Differentiable 𝕜 φ ∧ Differentiable 𝕜 φs :=
by
rw [differentiable_pi, Fin.forall_fin_succ, differentiable_pi]
simp only [Fin.cons_zero, Fin.cons_succ]
