Theorems · Theorem · measure theory

MeasureTheory.tendsto_measure_biInter_gt

∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_8} [inst : LinearOrder ι]
  [inst_1 : TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι] {s : ι → Set α} {a : ι},
  (∀ r > a, MeasureTheory.NullMeasurableSet (s r) μ) →
    (∀ (i j : ι), a < i → i ≤ j → s i ⊆ s j) →
      (∃ r > a, μ (s r) ≠ ⊤) → Filter.Tendsto (⇑μ ∘ s) (nhdsWithin a (Set.Ioi a)) (nhds (μ (⋂ r, ⋂ (_ : r > a), s r)))

The measure of the intersection of a decreasing sequence of measurable sets indexed by a linear order with first countable topology is the limit of the measures.

Defined in

Mathlib.MeasureTheory.Measure.MeasureSpace

Cited by

3 results in Mathlib

Foundations

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

Assumes

LinearOrderTopologicalSpaceOrderTopologyFirstCountableTopology