hasFDerivAt_pi — Mathlib

English

Differentiability of a map Φ: E → ∀ i, F'i is equivalent to differentiability of each coordinate Φ_i: E → F'i.

Русский

Дифференцируемость Φ: E → ∀ i, F'i эквивалентна дифференцируемости каждой координаты Φ_i: E → F'i.

LaTeX

$$$\\text{Differentiable } Φ \\iff \\forall i, \\text{Differentiable } Φ_i.$$$

Lean4

theorem hasFDerivAt_pi :
    HasFDerivAt (fun x i => φ i x) (ContinuousLinearMap.pi φ') x ↔ ∀ i, HasFDerivAt (φ i) (φ' i) x :=
  hasFDerivAtFilter_pi

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