Proportions of sets in outer measure

The proportion μ (s ∩ t) / μ t of a set s in a set t is at most one. This uses only monotonicity, so it is stated for OuterMeasureClass, which covers both outer measures and measures without requiring a measurable space.

Main results

• MeasureTheory.measure_inter_div_le_one

theorem MeasureTheory.measure_inter_div_le_one {α : Type u_1} {F : Type u_2} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] {μ : F} (s t : Set α) : μ (s ∩ t) / μ t ≤ 1

The proportion μ (s ∩ t) / μ t of a set s in a set t is at most one.