Theorems · Theorem · measure theory

MeasureTheory.measure_iUnion_congr_of_subset

∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Sort u_8} [Countable ι] {s t : ι → Set α},
  (∀ (i : ι), s i ⊆ t i) → (∀ (i : ι), μ (t i) ≤ μ (s i)) → μ (⋃ i, s i) = μ (⋃ i, t i)

Defined in

Mathlib.MeasureTheory.Measure.MeasureSpace

Cited by

2 results in Mathlib

Foundations

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

Assumes

Countable