Theorems · Theorem · measure theory

MeasureTheory.Measure.exists_measure_inter_spanningSets_pos

∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : MeasureTheory.SigmaFinite μ]
  (s : Set α), (∃ n, 0 < μ (s ∩ MeasureTheory.spanningSets μ n)) ↔ 0 < μ s

A set in a σ-finite space has positive measure if and only if its intersection with some member of the countable family of finite measure spanning sets has positive measure.

Defined in

Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasureTheory.SigmaFinite