hasFDerivAtFilter_pi — Mathlib

English

The HasFDerivAtFilter for a product-valued map is equivalent to the family of HasFDerivAtFilter for each coordinate, with the projection composed with Φ'.

Русский

Стандартная эквивалентность для произведения: производная по фильтру коэффициентов равна по всем координатам.

LaTeX

$$$\\HasFDerivAtFilter Φ Φ' x L \\iff ∀ i, HasFDerivAtFilter (fun x => Φ x i) ((proj i).comp Φ') x L.$$$

Lean4

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

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