English
The derivative of a product-valued map with respect to a filter factors coordinatewise: HasFDerivAtFilter Φ Φ' x L iff for all i HasFDerivAtFilter (fun x => Φ x i) ((proj i).comp Φ') x L.
Русский
Производная мапы с ценностью в произведении пространств по фильтру равна по координатам: HasFDerivAtFilter Φ Φ' x L тогда и только тогда, когда для всех i имеет место HasFDerivAtFilter (Φ x i) ((proj i) ∘ Φ') x L.
LaTeX
$$$\\HasFDerivAtFilter \\ Φ \\ Φ' \\ x \\ L \\iff \\forall i, HasFDerivAtFilter (fun x => Φ x i) ((proj i) \\circ Φ') \\ x \\ L.$$$
Lean4
@[simp]
theorem hasFDerivAtFilter_pi' :
HasFDerivAtFilter Φ Φ' x L ↔ ∀ i, HasFDerivAtFilter (fun x => Φ x i) ((proj i).comp Φ') x L :=
by
simp only [hasFDerivAtFilter_iff_isLittleO]
exact isLittleO_pi
