differentiableOn_finCons — Mathlib

English

On a set s, differentiability of Fin.cons is equivalent to differentiability of φ and φs on s.

Русский

На множестве s дифференцируемость Fin.cons равна дифференцируемости φ и φ_s на s.

LaTeX

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

Lean4

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

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