Theorems · Definition · measure theory
MeasureTheory.ComplexMeasure.equivSignedMeasure
{α : Type u_1} →
{m : MeasurableSpace α} →
MeasureTheory.ComplexMeasure α ≃ MeasureTheory.SignedMeasure α × MeasureTheory.SignedMeasure αThe complex measures form an equivalence to the type of pairs of signed measures.
- Defined in
- Mathlib.MeasureTheory.Measure.Complex
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 175 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- MeasurableSpacestatement and proof · cited by 13,106
- Equivstatement · cited by 8,337
- MeasureTheory.SignedMeasurestatement and proof · cited by 108
- MeasureTheory.ComplexMeasurestatement and proof · cited by 13
- MeasureTheory.SignedMeasure.toComplexMeasureproof · cited by 8
- MeasureTheory.ComplexMeasure.improof · cited by 7
- MeasureTheory.ComplexMeasure.reproof · cited by 7
- MeasureTheory.ComplexMeasure.toComplexMeasure_to_signedMeasureproof · cited by 1
Cited by5
Results whose statement or proof uses this declaration.
- MeasureTheory.ComplexMeasure.equivSignedMeasureₗproof · cited by 2
- MeasureTheory.ComplexMeasure.equivSignedMeasureₗ_symm_applystatement · cited by 0
- MeasureTheory.ComplexMeasure.equivSignedMeasure_applystatement and proof · cited by 0
- MeasureTheory.ComplexMeasure.equivSignedMeasure_symm_applystatement and proof · cited by 0
- MeasureTheory.ComplexMeasure.equivSignedMeasureₗ_applystatement · cited by 0