contDiffAt_piLp_apply

Mathlib.Analysis.Calculus.ContDiff.WithLp

URI: https://scilib.ai/kg/mathlib#contDiffAt_piLp_apply

← MathLib Explorer

English

The i-th coordinate projection is ContDiffWithinAt.

Русский

i-я координатная проекция является ContDiffWithinAt.

LaTeX

$$$ contDiffWithinAt\ 𝕜 n (f \mapsto f i) t y $$$

Lean4

@[fun_prop]
theorem contDiffAt_piLp_apply {i : ι} {y : PiLp p E} : ContDiffAt 𝕜 n (fun f : PiLp p E => f i) y :=
  (contDiffAt_piLp p).1 contDiffAt_id i

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru