finCons — Mathlib

English

Variant: DifferentiableAt (Fin.cons (φ x) (φs x)) iff φ and φs are differentiable at x.

Русский

Утверждение: дифференцируемость Fin.cons эквивалентна дифференцируемости компонент.

LaTeX

$$$\\text{DifferentiableAt}_{\\mathbb{K}}(\\lambda x.\\mathrm{Fin.cons}(\\phi x)(\\phi_s x)) x \\iff \\text{DifferentiableAt}_{\\mathbb{K}}(\\phi) x ∧ \\text{DifferentiableAt}_{\\mathbb{K}}(\\phi_s) x$$$

Lean4

@[fun_prop]
theorem finCons (h : DifferentiableWithinAt 𝕜 φ s x) (hs : DifferentiableWithinAt 𝕜 φs s x) :
    DifferentiableWithinAt 𝕜 (fun x => Fin.cons (φ x) (φs x)) s x :=
  differentiableWithinAt_finCons'.mpr ⟨h, hs⟩

Похожие утверждения