Source indexedlemma · leanprover/lean4:v4.32.0

Measure.Subtype.sigmaFinite

Carleson.ToMathlib.MeasureTheory.Measure.NNReal · Carleson/ToMathlib/MeasureTheory/Measure/NNReal.lean:107 to 129

Mathematical statement

Exact Lean statement

lemma Measure.Subtype.sigmaFinite {δ : Type*} [MeasureSpace δ] [sf : SigmaFinite (@volume δ _)] {p : δ → Prop} (hp : MeasurableSet p) :
    SigmaFinite (Measure.Subtype.measureSpace.volume : Measure (Subtype p)) where
  out'

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma Measure.Subtype.sigmaFinite {δ : Type*} [MeasureSpace δ] [sf : SigmaFinite (@volume δ _)] {p : δ → Prop} (hp : MeasurableSet p) :    SigmaFinite (Measure.Subtype.measureSpace.volume : Measure (Subtype p)) where  out' := by    refine Nonempty.intro ?_    rw [sigmaFinite_iff] at sf    rcases Classical.choice sf with ⟨set, set_mem, finite, spanning⟩    set set' := fun n ↦ (Subtype.val ⁻¹' (set n))    apply Measure.FiniteSpanningSetsIn.mk set'    · simp    · intro n      calc _        _ = volume (Subtype.val '' set' n) := by          apply comap_subtype_coe_apply hp volume (set' n)        _ ≤ volume (set n) := by          apply measure_mono          unfold set'          exact image_preimage_subset Subtype.val (set n)        _ < ⊤ := finite n    · unfold set'      rw [← preimage_iUnion]      refine preimage_eq_univ_iff.mpr ?_      rw [spanning]      exact fun ⦃a⦄ a ↦ trivial