Theorems · Theorem · measure theory
AddCircle.measure_univ
∀ (T : ℝ) [hT : Fact (0 < T)], MeasureTheory.volume Set.univ = ENNReal.ofReal T
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 182 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Fact
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Setstatement and proof · cited by 53,352
- Realstatement and proof · cited by 25,697
- MeasureTheory.Measurestatement · cited by 10,939
- ENNRealstatement · cited by 9,879
- Top.topproof · cited by 9,680
- Set.univstatement · cited by 3,945
- mul_oneproof · cited by 3,885
- Factstatement and proof · cited by 2,726
- MeasureTheory.MeasureSpace.volumestatement · cited by 1,323
- ENNReal.ofRealstatement and proof · cited by 863
- AddCirclestatement and proof · cited by 189
Cited by4
Results whose statement or proof uses this declaration.
- AddCircle.ae_empty_or_univ_of_forall_vadd_ae_eq_selfproof · cited by 2
- AddCircle.isAddFundamentalDomain_of_ae_ballproof · cited by 1
- UnitAddCircle.measure_univproof · cited by 0
- AddCircle.exists_norm_nsmul_leproof · cited by 0