differentiableAt_finCons — Mathlib

English

Equivalence: DifferentiableAt 𝕜 (λ x. Fin.cons (φ x) (φs x)) x iff DifferentiableAt φ x and DifferentiableAt φs 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

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

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