measure_iInter — Mathlib

English

Continuity from above for a directed upward family of measurable 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 directed downwards countable family of measurable sets
is the infimum of the measures. -/
theorem _root_.Directed.measure_iInter [Countable ι] {s : ι → Set α} (h : ∀ i, NullMeasurableSet (s i) μ)
    (hd : Directed (· ⊇ ·) s) (hfin : ∃ i, μ (s i) ≠ ∞) : μ (⋂ i, s i) = ⨅ i, μ (s i) :=
  by
  rcases hfin with ⟨k, hk⟩
  have : ∀ t ⊆ s k, μ t ≠ ∞ := fun t ht => ne_top_of_le_ne_top hk (measure_mono ht)
  rw [← ENNReal.sub_sub_cancel hk (iInf_le (fun i => μ (s i)) k), ENNReal.sub_iInf, ←
    ENNReal.sub_sub_cancel hk (measure_mono (iInter_subset _ k)), ←
    measure_diff (iInter_subset _ k) (.iInter h) (this _ (iInter_subset _ k)), diff_iInter, Directed.measure_iUnion]
  · congr 1
    refine le_antisymm (iSup_mono' fun i => ?_) (iSup_mono fun i => le_measure_diff)
    rcases hd i k with ⟨j, hji, hjk⟩
    use j
    rw [← measure_diff hjk (h _) (this _ hjk)]
    gcongr
  · exact hd.mono_comp _ fun _ _ => diff_subset_diff_right

Похожие утверждения