Continuity of measure without monotonicity

Stream: general

[Etienne Marion]

Hello!
I recently needed the following result:

theorem tendsto_measure_iUnion_iUnion (f : ℕ → Set X) :
  Tendsto (fun N ↦ μ (⋃ n ∈ Finset.range N, f n)) atTop (nhds (μ (⋃ n, f n)))

This is true by docs#MeasureTheory.tendsto_measure_iUnion when you set s to be

fun N ↦ (⋃ n ∈ (Finset.range N), f n)

but I did not find a general statement of continuity from below which did not require some monotonicity or "directedness" of the family of sets used.

I ended up proving this:

theorem measure_iUnion_eq_iSup' {α ι : Type*} [MeasurableSpace α] {μ : Measure α}
    (r : ι → ι → Prop) (r_trans : Transitive r) [Countable ι] [IsDirected ι r]
    {f : ι → Set α} : μ (⋃ (i : ι), f i) = ⨆ (i : ι), μ (⋃ j ∈ {j | r j i}, f j)

Unlike docs#MeasureTheory.measure_iUnion_eq_iSup, I removed any assumption about the family of sets and added instead assumptions about the index. Do you think this would be worth having, or something of the same kind?

[Anatole Dedecker]

My instinct would be to say that these are easy consequences of the directed versions and docs#Set.biUnion_iUnion. But I’ll let measure theory experts decide wether or not it’s worth adding

[Floris van Doorn]

Related PR: #12447.
(I haven't look closely enough to see whether these are useful to add, or too similar to the existing lemmas)