const_val

Mathlib.MeasureTheory.Function.LpSpace.Indicator

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

English

On the whole space, indicatorConstLp(p, univ, measure_ne_top μ, c) coincides with the Lp-constant function.

Русский

На всей области indicatorConstLp(p, univ, μ, c) совпадает с константой Lp.

LaTeX

$$indicatorConstLp(p, \text{univ}, μ, c) = Lp.const p μ c.$$

Lean4

@[simp]
theorem const_val : (Lp.const p μ c).1 = AEEqFun.const α c :=
  rfl

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

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

Разделы

Аффилиация

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