ι : Type ?u.247709
inst✝ : Fintype ι
a : ℝ
⊢ ↑↑volume (Ioi a) = ⊤
ι : Type ?u.247709
inst✝ : Fintype ι
a : ℝ
⊢ ↑↑volume (Ici a) = ⊤
rw [← measure_congr Ioi_ae_eq_Ici]
no goals
ι : Type ?u.247709
inst✝ : Fintype ι
a : ℝ
⊢ ↑↑volume (Ioi a) = ⊤
simp