contDiffOn_piLp_apply — Mathlib

English

There is a projection map from PiLp p E to its i-th coordinate, which is ContDiffOn.

Русский

Существует проекция из PiLp p E на i-ую координату, которая является ContDiffOn.

LaTeX

$$$ contDiffOn_piLp_apply\ {i}\ : ContDiffOn 𝕜 n (fun f => f i) t y $$$

Lean4

@[fun_prop]
theorem contDiffOn_piLp_apply {i : ι} {t : Set (PiLp p E)} : ContDiffOn 𝕜 n (fun f : PiLp p E => f i) t :=
  (contDiffOn_piLp p).1 contDiffOn_id i

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