hasDerivAtFilter_pi — Mathlib

English

A pi-type has HasDerivAtFilter φ φ' x L iff for every coordinate i, HasDerivAtFilter (λ x, φ x i) (φ' i) x L.

Русский

Пусть φ: 𝕜 → ∀ i, E'_i. Тогда HasDerivAtFilter φ φ' x L эквивалентно тому, что для каждого i производная координаты φ x i существует в φ' i по HasDerivAtFilter.

LaTeX

$$$HasDerivAtFilter \phi \phi' x L \iff \forall i, HasDerivAtFilter (\lambda x, \phi x i) (\phi' i) x L$$$

Lean4

@[simp]
theorem hasDerivAtFilter_pi : HasDerivAtFilter φ φ' x L ↔ ∀ i, HasDerivAtFilter (fun x => φ x i) (φ' i) x L :=
  hasFDerivAtFilter_pi'

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