Theorems · Theorem · measure theory

AEMeasurable.enorm

∀ {β : Type u_2} {ε : Type u_5} [inst : MeasurableSpace ε] [inst_1 : TopologicalSpace ε] [inst_2 : ContinuousENorm ε]
  [OpensMeasurableSpace ε] [inst_4 : MeasurableSpace β] {f : β → ε} {μ : MeasureTheory.Measure β},
  AEMeasurable f μ → AEMeasurable (fun x => ‖f x‖ₑ) μ

Defined in

Mathlib.MeasureTheory.Constructions.BorelSpace.Metric

Cited by

4 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceContinuousENormOpensMeasurableSpaceMeasurableSpace