Theorems · Definition · measure theory

MeasureTheory.AEEqFun.compMeasurable

{α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      [inst : MeasurableSpace α] →
        {μ : MeasureTheory.Measure α} →
          [inst_1 : TopologicalSpace β] →
            [inst_2 : TopologicalSpace γ] →
              [inst_3 : MeasurableSpace β] →
                [TopologicalSpace.PseudoMetrizableSpace β] →
                  [BorelSpace β] →
                    [inst_6 : MeasurableSpace γ] →
                      [TopologicalSpace.PseudoMetrizableSpace γ] →
                        [OpensMeasurableSpace γ] →
                          [SecondCountableTopology γ] → (g : β → γ) → Measurable g → (α →ₘ[μ] β) → α →ₘ[μ] γ

Given a measurable function g : β → γ, and an almost everywhere equal function [f] : α →ₘ β, return the equivalence class of g ∘ f, i.e., the almost everywhere equal function [g ∘ f] : α →ₘ γ. This requires that γ has a second countable topology.

Defined in

Mathlib.MeasureTheory.Function.AEEqFun

Cited by

7 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceTopologicalSpaceMeasurableSpaceTopologicalSpace.PseudoMetrizableSpaceBorelSpaceMeasurableSpaceTopologicalSpace.PseudoMetrizableSpaceOpensMeasurableSpaceSecondCountableTopology