hasStrictFDerivAt_pi'' — Mathlib

English

If for every index i the i-th coordinate of Φ has a strict derivative Φ′_i at x, then Φ has a strict derivative Φ′ at x in the product space.

Русский

Если для каждого индекса i координата Φ имеет строгую производную Φ′_i в точке x, тогда Φ имеет строгую производную Φ′ в точке x в произведении пространств.

LaTeX

$$$\\big( \\forall i,\\ HasStrictFDerivAt (Φ_i) ((proj_i) \\circ Φ') x \\big) \\implies HasStrictFDerivAt Φ Φ' x.$$$

Lean4

@[fun_prop]
theorem hasStrictFDerivAt_pi'' (hφ : ∀ i, HasStrictFDerivAt (fun x => Φ x i) ((proj i).comp Φ') x) :
    HasStrictFDerivAt Φ Φ' x :=
  hasStrictFDerivAt_pi'.2 hφ

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