LeanMachineLearning exposition

MeasureTheory.measurable_comp_comap🔗

Minimal Lean file

measurable_comp_comap🔗

LemmaMeasureTheory.measurable_comp_comap
Details

No docstring.

🔗theorem
MeasureTheory.measurable_comp_comap.{u_1, u_2, u_3} {α : Type u_1}
  {β : Type u_2} {γ : Type u_3} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (f : α → β) {g : β → γ} (hg : Measurable g) :
  Measurable (g ∘ f)
MeasureTheory.measurable_comp_comap.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {γ : Type u_3} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (f : α → β)
  {g : β → γ} (hg : Measurable g) :
  Measurable (g ∘ f)

Code

lemma measurable_comp_comap (f : α → β) {g : β → γ} (hg : Measurable g) :
    Measurable[mβ.comap f] (g ∘ f)
Used by (10)

Actions: Source · Open Issue

Proof
by
  rw [measurable_iff_comap_le, ← MeasurableSpace.comap_comp]
  exact MeasurableSpace.comap_mono hg.comap_le