English
If φ and φs are differentiable within s, then the Fin-cons combination is differentiable within s.
Русский
Если φ и φ_s дифференцируемы внутри s, то Fin.cons образует дифференцируемое отображение внутри s.
LaTeX
$$$\\text{DifferentiableWithinAt}_{\\mathbb{K}}\\big(\\lambda x.\\mathrm{Fin.cons}(\\phi x)(\\phi_s x)\\big) s x \\iff \\text{DifferentiableWithinAt}_{\\mathbb{K}}(\\phi s) s x ∧ \\text{DifferentiableWithinAt}_{\\mathbb{K}}(\\phi_s) s x$$$
Lean4
/-- A variant of `differentiableWithinAt_finCons` where the derivative variables are free on the RHS
instead. -/
theorem differentiableWithinAt_finCons' :
DifferentiableWithinAt 𝕜 (fun x => Fin.cons (φ x) (φs x)) s x ↔
DifferentiableWithinAt 𝕜 φ s x ∧ DifferentiableWithinAt 𝕜 φs s x :=
differentiableWithinAt_finCons
