Theorems · Theorem · measure theory

Measurable.subset

∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace β] [Countable α] {s t : β → Set α},
  Measurable s → Measurable t → Measurable fun a => s a ⊆ t a

Defined in

Mathlib.MeasureTheory.MeasurableSpace.Constructions

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceCountable