coe_LpSubmodule

Mathlib.MeasureTheory.Function.LpSpace.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Lp.coe_LpSubmodule

English

The coercion from the LpSubmodule to the ambient additive subgroup is the identity.

Русский

Приведение из LpSubmodule в Lp есть тождественное отображение.

LaTeX

$$$coe\_LpSubmodule = rfl$$$

Lean4

theorem coe_LpSubmodule : (LpSubmodule 𝕜 E p μ).toAddSubgroup = Lp E p μ :=
  rfl

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

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

Разделы

Аффилиация

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