contDiff_single — Mathlib

English

For a fixed index i, the map Pi.single i is a differentiable function in the sense of ContDiff, with respect to a parameter k in WithTop ℕ∞.

Русский

Для фиксированного индекса i отображение Pi.single i является дифференцируемым в смысле ContDiff по параметру k в WithTop ℕ∞.

LaTeX

$$$\\operatorname{ContDiff} \\ \\text{(depending on } k, i)$$$

Lean4

theorem contDiff_single [DecidableEq ι] (k : WithTop ℕ∞) (i : ι) : ContDiff 𝕜 k (Pi.single i : F' i → ∀ i, F' i) :=
  contDiff_update k 0 i

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