English
A variant of the previous criterion, where the derivative data on the right-hand side are allowed to be free. The map x ↦ Fin.cons(φ x)(φs x) is differentiable precisely when φ and φs are differentiable.
Русский
Вариант предыдущего критерия, в котором данные производной на правой части допускаются произвольными. Отображение 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
/-- A variant of `differentiable_finCons` where the derivative variables are free on the RHS
instead. -/
theorem differentiable_finCons' :
Differentiable 𝕜 (fun x => Fin.cons (φ x) (φs x)) ↔ Differentiable 𝕜 φ ∧ Differentiable 𝕜 φs :=
differentiable_finCons
