Theorems · Theorem · measure theory

MeasureTheory.SimpleFunc.eapprox_comp

∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace γ] {f : γ → ENNReal} {g : α → γ}
  {n : ℕ},
  Measurable f →
    Measurable g → ⇑(MeasureTheory.SimpleFunc.eapprox (f ∘ g) n) = ⇑(MeasureTheory.SimpleFunc.eapprox f n) ∘ g

Defined in

Mathlib.MeasureTheory.Function.SimpleFunc

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpace