English
Continuity from below: for a monotone s, μ(⋃ i s_i) = ⨆ i μ(s_i).
Русский
Непрерывность снизу: для монотонной последовательности s_i верно μ(⋃ i s_i) = ⨆ i μ(s_i).
LaTeX
$$$ \mu(\bigcup_i s_i) = \big\uparrow_i μ(s_i) \,$$$
Lean4
/-- Continuity from below:
the measure of the union of a monotone family of sets is equal to the supremum of their measures.
The theorem assumes that the `atTop` filter on the index set is countably generated,
so it works for a family indexed by a countable type, as well as `ℝ`. -/
theorem _root_.Monotone.measure_iUnion [Preorder ι] [IsDirected ι (· ≤ ·)] [(atTop : Filter ι).IsCountablyGenerated]
{s : ι → Set α} (hs : Monotone s) : μ (⋃ i, s i) = ⨆ i, μ (s i) := by
cases isEmpty_or_nonempty ι with
| inl _ => simp
| inr _ =>
rcases exists_seq_monotone_tendsto_atTop_atTop ι with ⟨x, hxm, hx⟩
rw [← hs.iUnion_comp_tendsto_atTop hx, ← Monotone.iSup_comp_tendsto_atTop _ hx]
exacts [(hs.comp hxm).directed_le.measure_iUnion, fun _ _ h ↦ measure_mono (hs h)]
