Theorems · Theorem · measure theory

MeasureTheory.AECover.biInter_Ici_aecover

∀ {α : Type u_1} {ι : Type u_2} [Countable ι] [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : Preorder ι] {φ : ι → Set α},
  MeasureTheory.AECover μ Filter.atTop φ → MeasureTheory.AECover μ Filter.atTop fun n => ⋂ k ∈ Set.Ici n, φ k

Defined in

Mathlib.MeasureTheory.Integral.IntegralEqImproper

Cited by

1 results in Mathlib

Foundations

Depth 172 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CountableMeasurableSpacePreorder