differentiable_apply — Mathlib

English

For a family of spaces F'_i, the evaluation map that sends a function f to its i-th coordinate f(i) is differentiable.

Русский

Оценочная карта f ↦ f(i) для Π_i F'_i дифференцируема.

LaTeX

$$$\\text{Differentiable}_{\\mathbb{K}}\\big(\\lambda f: \\prod_{i}F'_i \\mapsto f(i)\\big)$$$

Lean4

@[fun_prop]
theorem differentiable_apply (i : ι) : Differentiable (𝕜 := 𝕜) (fun f : ∀ i, F' i => f i) := by intro x;
  apply differentiableAt_apply

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