indicatorConstLp_add — Mathlib

English

Equality of indicatorConstLp with the MemLp embedding for constants.

Русский

Равенство indicatorConstLp и MemLp-встройки для констант.

LaTeX

$$indicatorConstLp p hs hμs c = MemLp.toLp (s.indicator fun x => c) (memLp_indicator_const p hs c (Or.inr hμs))$$

Lean4

/-- A version of `Set.indicator_add` for `MeasureTheory.indicatorConstLp` -/
theorem indicatorConstLp_add {c' : E} :
    indicatorConstLp p hs hμs c + indicatorConstLp p hs hμs c' = indicatorConstLp p hs hμs (c + c') :=
  by
  simp_rw [indicatorConstLp, ← MemLp.toLp_add, indicator_add]
  rfl

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