theorem EuclideanSpace.volume_ball_pos {r : ℝ} {ι : Type u_1} [Fintype ι] [Nonempty ι] (x : EuclideanSpace ℝ ι) (hr : 0 < r) : 0 < MeasureTheory.volume (Metric.ball x r)

noncomputable def Fintype.ofSingletonOnly (α : Type u_2) [Subsingleton α] : Fintype α

Equations

• Fintype.ofSingletonOnly α = if h : Nonempty α then Fintype.ofSubsingleton (Classical.choice h) else Fintype.ofIsEmpty

theorem MeasureTheory.MeasureSpace.volume_subsingleton {α : Type u_2} [MeasureSpace α] {s : Set α} (hs : Subsingleton ↑s) [NoAtoms volume] : volume s = 0

theorem EuclideanSpace.ball_subsingleton {r : ℝ} {ι : Type u_1} [Fintype ι] [IsEmpty ι] (x : EuclideanSpace ℝ ι) : Subsingleton ↑(Metric.ball x r)

theorem EuclideanSpace.volume_ball_lt_top {r : ℝ} {ι : Type u_1} [Fintype ι] [inst : MeasureTheory.NoAtoms MeasureTheory.volume] (x : EuclideanSpace ℝ ι) : MeasureTheory.volume (Metric.ball x r) < ⊤