Theorems · Theorem · measure theory

MeasureTheory.StronglyMeasurable.ae_le_trim_of_stronglyMeasurable

∀ {α : Type u_1} {E : Type u_5} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → E}
  [inst : TopologicalSpace E] [inst_1 : Preorder E] [OrderClosedTopology E] [TopologicalSpace.PseudoMetrizableSpace E]
  (hm : m ≤ m₀), MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable g → f ≤ᵐ[μ] g → f ≤ᵐ[μ.trim hm] g

Defined in

Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpacePreorderOrderClosedTopologyTopologicalSpace.PseudoMetrizableSpace