differentiableOn_pi — Mathlib

English

If every coordinate function is differentiable, then the product map Φ is differentiable.

Русский

Если каждая координатная функция дифференцируема, то произведение дифференцируемо.

LaTeX

$$$\\forall i, \\text{Differentiable } Φ_i x \\Rightarrow \\text{Differentiable } Φ x.$$$

Lean4

theorem differentiableOn_pi : DifferentiableOn 𝕜 Φ s ↔ ∀ i, DifferentiableOn 𝕜 (fun x => Φ x i) s :=
  ⟨fun h i x hx => differentiableWithinAt_pi.1 (h x hx) i, fun h x hx => differentiableWithinAt_pi.2 fun i => h i x hx⟩

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