finCons — Mathlib

English

Variant: DifferentiableOn of Fin.cons with φ and φs yields a differentiable Fin.cons map on s.

Русский

Variant: дифференцируемость Fin.cons на s.

LaTeX

$$$\\text{DifferentiableOn}_{\\mathbb{K}}(\\lambda x.\\mathrm{Fin.cons}(\\phi x)(\\phi_s x)) s \\Rightarrow \\text{DifferentiableOn}_{\\mathbb{K}}(\\phi) s ∧ \\text{DifferentiableOn}_{\\mathbb{K}}(\\phi_s) s$$$

Lean4

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

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