Theorems · Definition · measure theory

MeasureTheory.Measure.FiniteSpanningSetsIn.casesOn

{α : Type u_1} →
  {m0 : MeasurableSpace α} →
    {μ : MeasureTheory.Measure α} →
      {C : Set (Set α)} →
        {motive : μ.FiniteSpanningSetsIn C → Sort u} →
          (t : μ.FiniteSpanningSetsIn C) →
            ((set : ℕ → Set α) →
                (set_mem : ∀ (i : ℕ), set i ∈ C) →
                  (finite : ∀ (i : ℕ), μ (set i) < ⊤) →
                    (spanning : ⋃ i, set i = Set.univ) →
                      motive { set := set, set_mem := set_mem, finite := finite, spanning := spanning }) →
              motive t

Defined in

Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Cited by

2 results in Mathlib

Foundations

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