Theorems · Theorem · measure theory

MeasureTheory.mem_lpMeas_self

∀ {α : Type u_1} {F : Type u_2} {𝕜 : Type u_3} {p : ENNReal} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : ↥(MeasureTheory.Lp F p μ)),
  f ∈ MeasureTheory.lpMeas F 𝕜 m0 p μ

Defined in

Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable

Cited by

0 results in Mathlib

Foundations

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

Assumes

RCLikeNormedAddCommGroupNormedSpace