hasFDerivWithinAt_pi'' — Mathlib

English

Any coordinate-wise strict differentiability implies the full HasFDerivWithinAt for the product map.

Русский

Любая координатная строгая дифференциация порождает полную HasFDerivWithinAt для произведения.

LaTeX

$$$\\text{HasFDerivWithinAt}(Φ, Φ', s, x) \\iff \\forall i, \\text{HasFDerivWithinAt}(Φ_i, Φ'_i, s, x).$$$

Lean4

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

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