contDiffOn_apply — Mathlib

English

For each i, the map f ↦ f(i) is ContDiffOn 𝕜 n on any set of functions.

Русский

Для каждого i отображение f ↦ f(i) является ContDiffOn 𝕜 n на произвольном множестве функций.

LaTeX

$$$\text{ContDiffOn } 𝕜 n (\lambda f: f(i)) \; s$$$

Lean4

@[fun_prop]
theorem contDiffOn_apply (i : ι) (s : Set (ι → E)) : ContDiffOn 𝕜 n (fun f : ι → E => f i) s :=
  (contDiff_apply 𝕜 E i).contDiffOn

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