differentiableAt_apply — Mathlib

English

Differentiability of a product-valued map is characterized by differentiability of each coordinate function.

Русский

Дифференцируемость отображения в произведение пространств характеризуется дифференцируемостью каждой координаты.

LaTeX

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

Lean4

@[fun_prop]
theorem differentiableAt_apply (i : ι) (f : ∀ i, F' i) : DifferentiableAt (𝕜 := 𝕜) (fun f : ∀ i, F' i => f i) f :=
  by
  have h := ((differentiableAt_pi (𝕜 := 𝕜) (Φ := fun (f : ∀ i, F' i) (i' : ι) => f i') (x := f))).1
  apply h; apply differentiableAt_id

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