English
Continuity from above for a countable directed family: μ(∩ f i) = inf μ(∩_{j ≤ i} f j) under null-measurability and finiteness conditions.
Русский
Постоянство по сверху для счётной направленной семьи: при условии нулевой измеримости и конечности, μ(⋂ f i) = inf_i μ(⋂_{j ≤ i} f j).
LaTeX
$$$\\mu\\left(\\bigcap_i f(i)\\right) = \\inf_i \\mu\\left(\\bigcap_{j \\le i} f(j)\\right)$$$
Lean4
/-- Continuity from above: the measure of the intersection of a sequence of
measurable sets is the infimum of the measures of the partial intersections. -/
theorem measure_iInter_eq_iInf_measure_iInter_le {α ι : Type*} {_ : MeasurableSpace α} {μ : Measure α} [Countable ι]
[Preorder ι] [IsDirected ι (· ≤ ·)] {f : ι → Set α} (h : ∀ i, NullMeasurableSet (f i) μ) (hfin : ∃ i, μ (f i) ≠ ∞) :
μ (⋂ i, f i) = ⨅ i, μ (⋂ j ≤ i, f j) := by
rw [← Antitone.measure_iInter]
· rw [iInter_comm]
exact congrArg μ <| iInter_congr fun i ↦ (biInf_const nonempty_Ici).symm
· exact fun i j h ↦ biInter_mono (Iic_subset_Iic.2 h) fun _ _ ↦ Set.Subset.rfl
· exact fun i ↦ .biInter (to_countable _) fun _ _ ↦ h _
· refine hfin.imp fun k hk ↦ ne_top_of_le_ne_top hk <| measure_mono <| iInter₂_subset k ?_
rfl
