differentiableWithinAt_finCons — Mathlib

English

A variant for HasFDerivAtFilter; if HasFDerivAtFilter φ φ' x l and HasFDerivAtFilter φs φs' x l then HasFDerivAtFilter (λ x => Fin.cons (φ x) (φs x)) (φ'.finCons φs') x l.

Русский

Вариант HasFDerivAtFilter.

LaTeX

$$$HasFDerivAtFilter\\phi\\phi' x l ∧ HasFDerivAtFilter\\phi_s\\phi_s' x l \\Rightarrow HasFDerivAtFilter\\big(\\lambda x.\\mathrm{Fin.cons}(\\phi x)(\\phi_s x)\\big) (\\phi'.finCons φs') x l$$

Lean4

theorem differentiableWithinAt_finCons :
    DifferentiableWithinAt 𝕜 (fun x => Fin.cons (φ x) (φs x)) s x ↔
      DifferentiableWithinAt 𝕜 φ s x ∧ DifferentiableWithinAt 𝕜 φs s x :=
  by
  rw [differentiableWithinAt_pi, Fin.forall_fin_succ, differentiableWithinAt_pi]
  simp only [Fin.cons_zero, Fin.cons_succ]

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