Theorems · Definition · measure theory
MeasureTheory.VectorMeasure.equivMeasure
{α : Type u_1} → [inst : MeasurableSpace α] → MeasureTheory.VectorMeasure α ENNReal ≃ MeasureTheory.Measure αThe equiv between VectorMeasure α ℝ≥0∞ and Measure α formed by
MeasureTheory.VectorMeasure.ennrealToMeasure and
MeasureTheory.Measure.toENNRealVectorMeasure.
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 176 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- MeasurableSpace
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.
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement · cited by 10,939
- ENNRealstatement · cited by 9,879
- Equivstatement · cited by 8,337
- MeasureTheory.VectorMeasurestatement · cited by 451
- MeasureTheory.Measure.toENNRealVectorMeasureproof · cited by 18
- MeasureTheory.VectorMeasure.ennrealToMeasureproof · cited by 13
- MeasureTheory.VectorMeasure.ennrealToMeasure_toENNRealVectorMeasureproof · cited by 2
- MeasureTheory.Measure.toENNRealVectorMeasure_ennrealToMeasureproof · cited by 1
Cited by3
Results whose statement or proof uses this declaration.
- MeasureTheory.SignedMeasure.withDensityᵥ_rnDeriv_eqproof · cited by 2
- MeasureTheory.VectorMeasure.equivMeasure_applystatement and proof · cited by 0
- MeasureTheory.VectorMeasure.equivMeasure_symm_applystatement and proof · cited by 0