hasFDerivAt_pi' — Mathlib

English

HasStrictFDerivAt of Φ from x into a Pi-space is equivalent to HasStrictFDerivAt of each coordinate with the coordinate-specific Φ′.

Русский

Строгая производная Φ в точке x в Pi-пространстве эквивалентна строгой производной каждой coordinate, с использованием соответствующей Φ′.

LaTeX

$$$\\text{HasStrictFDerivAt } Φ Φ' x \\iff \\forall i, \\ HasStrictFDerivAt (Φ_i) (Φ'_i) x.$$$

Lean4

@[simp]
theorem hasFDerivAt_pi' : HasFDerivAt Φ Φ' x ↔ ∀ i, HasFDerivAt (fun x => Φ x i) ((proj i).comp Φ') x :=
  hasFDerivAtFilter_pi'

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