English
If φ and φs are differentiable, then the finite-cons map x ↦ Fin.cons(φ x)(φs x) is differentiable.
Русский
Если φ и φs дифференцируемы, то отображение x ↦ Fin.cons(φ x)(φs x) в конечное произведение дифференцируемо.
LaTeX
$$$ \operatorname{Differentiable}_{\mathbb{k}}(\lambda x:\,E\;\mapsto\; \mathrm{Fin.cons}(\phi x)(\phi_s x)) = \operatorname{Differentiable}_{\mathbb{k}}(\phi) \wedge \operatorname{Differentiable}_{\mathbb{k}}(\phi_s) \; \Rightarrow \; \operatorname{Differentiable}_{\mathbb{k}}(\lambda x:\,E\;\mapsto\; \mathrm{Fin.cons}(\phi x)(\phi_s x)). $$$
Lean4
@[fun_prop]
theorem finCons (h : Differentiable 𝕜 φ) (hs : Differentiable 𝕜 φs) :
Differentiable 𝕜 (fun x => Fin.cons (φ x) (φs x)) :=
differentiable_finCons'.mpr
⟨h, hs⟩
-- TODO: write the `Fin.cons` versions of `fderivWithin_pi` and `fderiv_pi`
