hasStrictDerivAt_pi — Mathlib

English

A pi-type has strict derivative φ' at x iff each coordinate φ x i has strict derivative φ' i at x, for finite index set.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem hasStrictDerivAt_pi : HasStrictDerivAt φ φ' x ↔ ∀ i, HasStrictDerivAt (fun x => φ x i) (φ' i) x :=
  hasStrictFDerivAt_pi'

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