hasDerivWithinAt_pi — Mathlib

English

A pi-type φ has HasDerivWithinAt φ φ' s x iff for all i, HasDerivWithinAt (λ x, φ x i) (φ' i) s x.

Русский

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

LaTeX

$$$HasDerivWithinAt \phi \phi' s x \iff \forall i, HasDerivWithinAt (\\lambda x, \\phi x i) (\\phi' i) s x$$$

Lean4

theorem hasDerivWithinAt_pi : HasDerivWithinAt φ φ' s x ↔ ∀ i, HasDerivWithinAt (fun x => φ x i) (φ' i) s x :=
  hasDerivAtFilter_pi

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