ι : Type u_2
α : Type u_1
β : Type ?u.8694
γ : Type ?u.8697
m0✝ : MeasurableSpace α
μ✝ : Measure α
s t : Set α
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
f : ι → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : ι), MeasurableSet (f i)
⊢ (∑' (i : ι), extend (fun t _ht => ↑↑μ t) (f i)) = ∑' (i : ι), ↑↑μ (f i)

ι : Type u_2
α : Type u_1
β : Type ?u.8694
γ : Type ?u.8697
m0✝ : MeasurableSpace α
μ✝ : Measure α
s t : Set α
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
f : ι → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : ι), MeasurableSet (f i)
⊢ ↑↑μ ∅ = 0

ι : Type u_2
α : Type u_1
β : Type ?u.8694
γ : Type ?u.8697
m0✝ : MeasurableSpace α
μ✝ : Measure α
s t : Set α
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
f : ι → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : ι), MeasurableSet (f i)
⊢ ∀ ⦃f : ℕ → Set α⦄,
    (∀ (i : ℕ), MeasurableSet (f i)) → Pairwise (Disjoint on f) → ↑↑μ (⋃ (i : ℕ), f i) = ∑' (i : ℕ), ↑↑μ (f i)
ι : Type u_2
α : Type u_1
β : Type ?u.8694
γ : Type ?u.8697
m0✝ : MeasurableSpace α
μ✝ : Measure α
s t : Set α
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
f : ι → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : ι), MeasurableSet (f i)
⊢ ↑↑μ (⋃ (i : ι), f i) = ∑' (i : ι), ↑↑μ (f i)
rw [measure_eq_extend (MeasurableSet.iUnion h),
  extend_iUnion MeasurableSet.empty _ MeasurableSet.iUnion _ hn h]
no goals
ι : Type u_2
α : Type u_1
β : Type ?u.8694
γ : Type ?u.8697
m0✝ : MeasurableSpace α
μ✝ : Measure α
s t : Set α
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
f : ι → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : ι), MeasurableSet (f i)
⊢ (∑' (i : ι), extend (fun t _ht => ↑↑μ t) (f i)) = ∑' (i : ι), ↑↑μ (f i)
simp [measure_eq_extend, h]
no goals
ι : Type u_2
α : Type u_1
β : Type ?u.8694
γ : Type ?u.8697
m0✝ : MeasurableSpace α
μ✝ : Measure α
s t : Set α
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
f : ι → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : ι), MeasurableSet (f i)
⊢ ↑↑μ ∅ = 0
exact μ.empty
no goals
ι : Type u_2
α : Type u_1
β : Type ?u.8694
γ : Type ?u.8697
m0✝ : MeasurableSpace α
μ✝ : Measure α
s t : Set α
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
f : ι → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : ι), MeasurableSet (f i)
⊢ ∀ ⦃f : ℕ → Set α⦄,
    (∀ (i : ℕ), MeasurableSet (f i)) → Pairwise (Disjoint on f) → ↑↑μ (⋃ (i : ℕ), f i) = ∑' (i : ℕ), ↑↑μ (f i)
exact μ.m_iUnion