English
If a family of sets has finite-measure at some stage and each f_i is null-measurable, then μ(⋂ i, f_i) equals the limit of μ(⋂_{j≤i} f_j).
Русский
При условии существования некоторой конечной меры μ(f_i) и нулевой измеримости каждого f_i, мера ⋂_i f_i равна пределу μ(⋂_{j≤i} f_j).
LaTeX
$$$$\forall i,\ NullMeasurableSet(f_i,\mu) \Rightarrow \mathrm{Tendsto}(i \mapsto μ(\bigcap_{j\le i} f_j))\ atTop\ (\mathcal{N}(μ(\bigcap_i f_i))).$$$$
Lean4
/-- Continuity from above: the measure of the intersection of a sequence of measurable
sets such that one has finite measure is the limit of the measures of the partial intersections. -/
theorem tendsto_measure_iInter_le {α ι : Type*} {_ : MeasurableSpace α} {μ : Measure α} [Countable ι] [Preorder ι]
{f : ι → Set α} (hm : ∀ i, NullMeasurableSet (f i) μ) (hf : ∃ i, μ (f i) ≠ ∞) :
Tendsto (fun i ↦ μ (⋂ j ≤ i, f j)) atTop (𝓝 (μ (⋂ i, f i))) :=
by
refine .of_neBot_imp fun hne ↦ ?_
cases atTop_neBot_iff.mp hne
rw [measure_iInter_eq_iInf_measure_iInter_le hm hf]
exact tendsto_atTop_iInf fun i j hij ↦ measure_mono <| biInter_subset_biInter_left fun k hki ↦ le_trans hki hij
