hasStrictFDerivAt_pi — Mathlib

English

The statement that HasStrictFDerivAt Φ Φ' x is equivalent to coordinatewise HasStrictFDerivAt for each i, i.e., Φ′_i = (proj i) ∘ Φ'.

Русский

Утверждение, что строгая производная Φ в x эквивалентна по координатам для каждого i: Φ′_i = (proj i) ∘ Φ'.

LaTeX

$$$\\HasStrictFDerivAt Φ Φ' x \\iff \\forall i, HasStrictFDerivAt (Φ x i) ((proj i) \\circ Φ') x.$$$

Lean4

theorem hasStrictFDerivAt_pi :
    HasStrictFDerivAt (fun x i => φ i x) (ContinuousLinearMap.pi φ') x ↔ ∀ i, HasStrictFDerivAt (φ i) (φ' i) x :=
  hasStrictFDerivAt_pi'

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