Theorems · Theorem · measure theory

EuclideanSpace.volume_closedBall

∀ (ι : Type u_1) [Nonempty ι] [inst : Fintype ι] (x : EuclideanSpace ℝ ι) (r : ℝ),
  MeasureTheory.volume (Metric.closedBall x r) =
    ENNReal.ofReal r ^ Fintype.card ι *
      ENNReal.ofReal (√Real.pi ^ Fintype.card ι / Real.Gamma (↑(Fintype.card ι) / 2 + 1))

Defined in: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Cited by: 0 results in Mathlib
Foundations: Depth 295 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Nonempty Fintype

Mathlib docs Source Loogle LeanSearch

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 · cited by 62,936
Setstatement · cited by 53,352
Realstatement and proof · cited by 25,697
MeasureTheory.Measurestatement · cited by 10,939
ENNRealstatement and proof · cited by 9,879
Fintypestatement and proof · cited by 7,736
Real.pistatement and proof · cited by 1,774
Fintype.cardstatement and proof · cited by 1,386
MeasureTheory.MeasureSpace.volumestatement and proof · cited by 1,323
ENNReal.ofRealstatement and proof · cited by 863
Metric.closedBallstatement · cited by 704
Real.sqrtstatement and proof · cited by 545

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.