coeFn_const

Mathlib.MeasureTheory.Function.LpSpace.Indicator

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

English

Consider the map c ↦ indicatorConstLp(p, hs, hμs, c). This is linear in c, hence defines a linear map from E to Lp.

Русский

Пусть c ↦ indicatorConstLp(p, hs, hμs, c). Это линейно по c, поэтому задаёт линейное отображение E → Lp.

LaTeX

$$indicatorConstLp(p, hs, hμs, ·) : E → Lp E p μ is linear.$$

Lean4

theorem coeFn_const : Lp.const p μ c =ᵐ[μ] Function.const α c :=
  AEEqFun.coeFn_const α c

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

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

Разделы

Аффилиация

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