Theorems · Definition · measure theory

MeasureTheory.ComplexMeasure.HaveLebesgueDecomposition.casesOn

{α : Type u_1} →
  {m : MeasurableSpace α} →
    {c : MeasureTheory.ComplexMeasure α} →
      {μ : MeasureTheory.Measure α} →
        {motive : c.HaveLebesgueDecomposition μ → Sort u} →
          (t : c.HaveLebesgueDecomposition μ) →
            ((rePart : (MeasureTheory.ComplexMeasure.re c).HaveLebesgueDecomposition μ) →
                (imPart : (MeasureTheory.ComplexMeasure.im c).HaveLebesgueDecomposition μ) → motive ⋯) →
              motive t

Defined in

Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Cited by

0 results in Mathlib

Foundations

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