differentiableAt_finCons' — Mathlib

English

Variant: DifferentiableAt (Fin.cons ...) is equivalent to the pair of differentiabilities of φ and φs.

Русский

Вариант: дифференцируемость Fin.cons эквивалентна паре дифференцируемостей φ и φ_s.

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

/-- A variant of `differentiableAt_finCons` where the derivative variables are free on the RHS
instead. -/
theorem differentiableAt_finCons' :
    DifferentiableAt 𝕜 (fun x => Fin.cons (φ x) (φs x)) x ↔ DifferentiableAt 𝕜 φ x ∧ DifferentiableAt 𝕜 φs x :=
  differentiableAt_finCons

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