Measurability lemmas

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

theorem MeasureTheory.MeasurableSet.imp {α : Type u_1} {mα : MeasurableSpace α} {p q : α → Prop} (hs : MeasurableSet {x : α | p x}) (ht : MeasurableSet {x : α | q x}) : MeasurableSet {x : α | p x → q x}

theorem MeasureTheory.MeasurableSet.iff {α : Type u_1} {mα : MeasurableSpace α} {p q : α → Prop} (hs : MeasurableSet {x : α | p x}) (ht : MeasurableSet {x : α | q x}) : MeasurableSet {x : α | p x ↔ q x}