hasDerivAt_pi — Mathlib

English

A pi-type φ has HasDerivAt φ φ' x if and only if each coordinate has HasDerivAt (coordinate function).

Русский

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

LaTeX

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

Lean4

theorem hasDerivAt_pi : HasDerivAt φ φ' x ↔ ∀ i, HasDerivAt (fun x => φ x i) (φ' i) x :=
  hasDerivAtFilter_pi

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