Theorems · Theorem · measure theory

MeasurableSpace.comap_le_comap_of_eq_comp

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : α → β} {g : α → γ}
  (h : β → γ), Measurable h → g = h ∘ f → MeasurableSpace.comap g mγ ≤ MeasurableSpace.comap f mβ

If g = h ∘ f, then the sigma-algebra generated by g is smaller than the one generated by f.

Defined in

Mathlib.MeasureTheory.MeasurableSpace.Basic

Cited by

0 results in Mathlib

Foundations

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