English
Continuity from above for an antitone family indexed by a countably generated atTop filter, yielding an infimum of measures.
Русский
Непрерывность сверху для антитонной последовательности с учётом счётной генерации фильтра atTop, приводящая к инфиму мер.
LaTeX
$$$ μ(\bigcap_i s_i) = \inf_i μ(s_i) $$$
Lean4
/-- **Continuity from above**:
the measure of the intersection of an antitone family of measurable sets
indexed by a type with countably generated `atTop` filter
is equal to the infimum of the measures. -/
theorem _root_.Antitone.measure_iInter [Preorder ι] [IsDirected ι (· ≤ ·)] [(atTop : Filter ι).IsCountablyGenerated]
{s : ι → Set α} (hs : Antitone s) (hsm : ∀ i, NullMeasurableSet (s i) μ) (hfin : ∃ i, μ (s i) ≠ ∞) :
μ (⋂ i, s i) = ⨅ i, μ (s i) :=
hs.dual_left.measure_iInter hsm hfin
