case hsum
α : Type u_1
β : Type ?u.645610
γ : Type ?u.645613
δ : Type ?u.645616
ι : Type ?u.645619
R : Type ?u.645622
R' : Type ?u.645625
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ (∑' (x : ℕ), ↑↑μ (f x)) ≠ ⊤
α : Type u_1
β : Type ?u.645610
γ : Type ?u.645613
δ : Type ?u.645616
ι : Type ?u.645619
R : Type ?u.645622
R' : Type ?u.645625
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ Summable fun x => ENNReal.toReal (↑↑μ (f x))
apply ENNReal.summable_toReal
case hsum
α : Type u_1
β : Type ?u.645610
γ : Type ?u.645613
δ : Type ?u.645616
ι : Type ?u.645619
R : Type ?u.645622
R' : Type ?u.645625
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ ↑↑μ (⋃ (i : ℕ), f i) ≠ ⊤
case hsum
α : Type u_1
β : Type ?u.645610
γ : Type ?u.645613
δ : Type ?u.645616
ι : Type ?u.645619
R : Type ?u.645622
R' : Type ?u.645625
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ (∑' (x : ℕ), ↑↑μ (f x)) ≠ ⊤
rw [← MeasureTheory.measure_iUnion hf₂ hf₁]
no goals
case hsum
α : Type u_1
β : Type ?u.645610
γ : Type ?u.645613
δ : Type ?u.645616
ι : Type ?u.645619
R : Type ?u.645622
R' : Type ?u.645625
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ ↑↑μ (⋃ (i : ℕ), f i) ≠ ⊤
exact ne_of_lt (measure_lt_top _ _)