Theorems · Theorem · measure theory

MeasureTheory.indicatorConstLp_eq_toSpanSingleton_compLp

∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  {s : Set α} [inst_1 : NormedSpace ℝ E] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : E),
  MeasureTheory.indicatorConstLp 2 hs hμs x =
    (ContinuousLinearMap.toSpanSingleton ℝ x).compLp (MeasureTheory.indicatorConstLp 2 hs hμs 1)

Defined in

Mathlib.MeasureTheory.Function.LpSpace.Indicator

Cited by

1 results in Mathlib

Foundations

Depth 228 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace