coe_lpBCFₗᵢ

Mathlib.Analysis.Normed.Lp.LpEquiv

URI: https://scilib.ai/kg/mathlib#coe_lpBCFₗᵢ

English

The underlying function of the canonical equivalence is the identity on the function space.

Русский

Базовая функция канонического эквиверенца совпадает с исходной функцией.

LaTeX

$$$(lpPiLp f) = f$$$

Lean4

theorem coe_lpBCFₗᵢ (f : lp (fun _ : α ↦ E) ∞) : (lpBCFₗᵢ E 𝕜 f : α → E) = f :=
  rfl

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

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

Разделы

Аффилиация

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