English
Continuity from above for a monotone family of sets: μ(⋂ s_i) = ⨅ μ(s_i).
Русский
Непрерывность сверху для монотонного семейства множеств: μ(⋂ s_i) = ⨅ μ(s_i).
LaTeX
$$$ μ(\bigcap_i s_i) = \inf_i μ(s_i) $$$
Lean4
/-- **Continuity from above**:
the measure of the intersection of a monotone family of measurable sets
indexed by a type with countably generated `atBot` filter
is equal to the infimum of the measures. -/
theorem _root_.Monotone.measure_iInter [Preorder ι] [IsDirected ι (· ≥ ·)] [(atBot : Filter ι).IsCountablyGenerated]
{s : ι → Set α} (hs : Monotone s) (hsm : ∀ i, NullMeasurableSet (s i) μ) (hfin : ∃ i, μ (s i) ≠ ∞) :
μ (⋂ i, s i) = ⨅ i, μ (s i) :=
by
refine le_antisymm (le_iInf fun i ↦ measure_mono <| iInter_subset _ _) ?_
have := hfin.nonempty
rcases exists_seq_antitone_tendsto_atTop_atBot ι with ⟨x, hxm, hx⟩
calc
⨅ i, μ (s i) ≤ ⨅ n, μ (s (x n)) := le_iInf_comp (μ ∘ s) x
_ = μ (⋂ n, s (x n)) :=
by
refine .symm <| (hs.comp_antitone hxm).directed_ge.measure_iInter (fun n ↦ hsm _) ?_
rcases hfin with ⟨k, hk⟩
rcases (hx.eventually_le_atBot k).exists with ⟨n, hn⟩
exact ⟨n, ne_top_of_le_ne_top hk <| measure_mono <| hs hn⟩
_ ≤ μ (⋂ i, s i) := by
refine measure_mono <| iInter_mono' fun i ↦ ?_
rcases (hx.eventually_le_atBot i).exists with ⟨n, hn⟩
exact ⟨n, hs hn⟩
