differentiable_pi'' — Mathlib

English

Let Φ be a map from a normed space E into a product ∏_{i∈ι} F'_i. If every coordinate map x ↦ Φ(x)_i is differentiable, then Φ is differentiable.

Русский

Пусть Φ: E → ∏_{i∈ι} F'_i. Если каждая координатная функция x ↦ Φ(x)_i дифференцируема, то Φ дифференцируема.

LaTeX

$$$\\Big(\\forall i, \\text{Differentiable}_{\\mathbb{K}}(x \\mapsto \\Phi(x)_i)\\Big) \\Rightarrow \\text{Differentiable}_{\\mathbb{K}}(\\Phi)$$$

Lean4

@[fun_prop]
theorem differentiable_pi'' (hφ : ∀ i, Differentiable 𝕜 fun x => Φ x i) : Differentiable 𝕜 Φ :=
  differentiable_pi.2 hφ

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