ι : Type u_1
inst✝¹ : Finite ι
I : Box ι
π : Prepartition I
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ ∀ (b : Box ι), b ∈ π.boxes → MeasurableSet ↑b

ι : Type u_1
inst✝¹ : Finite ι
I : Box ι
π : Prepartition I
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ ∀ (a : Box ι), a ∈ π.boxes → ↑↑μ ↑a ≠ ⊤
ι : Type u_1
inst✝¹ : Finite ι
I : Box ι
π : Prepartition I
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ ENNReal.toReal (↑↑μ (Prepartition.iUnion π)) = ∑ J in π.boxes, ENNReal.toReal (↑↑μ ↑J)
erw [← ENNReal.toReal_sum, π.iUnion_def, measure_biUnion_finset π.pairwiseDisjoint]
no goals
ι : Type u_1
inst✝¹ : Finite ι
I : Box ι
π : Prepartition I
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ ∀ (b : Box ι), b ∈ π.boxes → MeasurableSet ↑b

ι : Type u_1
inst✝¹ : Finite ι
I : Box ι
π : Prepartition I
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ ∀ (a : Box ι), a ∈ π.boxes → ↑↑μ ↑a ≠ ⊤
exacts [fun J _ => J.measurableSet_coe, fun J _ => (J.measure_coe_lt_top μ).ne]