toLp_const — Mathlib

English

The coeFn and the Lp const interact nicely, giving a canonical identification between indicatorConstLp on univ and Lp.const.

Русский

Коэрфункция и константа Lp хорошо взаимодействуют, образуя каноническое соответствие индикаторного IndConst на всём множестве и Lp.const.

LaTeX

$$indicatorConstLp p univ (measure_ne_top μ) c = Lp.const p μ c$$

Lean4

@[simp]
theorem toLp_const : MemLp.toLp _ (memLp_const c) = Lp.const p μ c :=
  rfl

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