ι : Type ?u.252971
inst✝ : Fintype ι
a : ℝ
⊢ ↑↑volume (Iio a) = ⊤
ι : Type ?u.252971
inst✝ : Fintype ι
a : ℝ
⊢ ↑↑volume (Iic a) = ⊤
rw [← measure_congr Iio_ae_eq_Iic]
no goals
ι : Type ?u.252971
inst✝ : Fintype ι
a : ℝ
⊢ ↑↑volume (Iio a) = ⊤
simp