indicatorConstLp_univ — Mathlib

English

As a simp lemma, indicatorConstLp on the universal set equals the Lp-constant function.

Русский

Как простая лемма, indicatorConstLp на всём множестве равен константе Lp.

LaTeX

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

Lean4

@[simp]
theorem indicatorConstLp_univ : indicatorConstLp p .univ (measure_ne_top μ _) c = Lp.const p μ c :=
  by
  rw [← MemLp.toLp_const, indicatorConstLp]
  simp only [Set.indicator_univ]

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