case intro
α : Type u_2
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) = ∑' (i : ℕ), m (f i) (_ : P (f i))
msU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) ≤ ∑' (i : ℕ), m (f i) (_ : P (f i))
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
β : Type u_1
inst✝ : Countable β
f : β → Set α
hd : Pairwise (Disjoint on f)
hm : ∀ (i : β), P (f i)
val✝ : Encodable β
⊢ extend m (⋃ (i : β), f i) = ∑' (i : β), extend m (f i)
α : Type u_2
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) = ∑' (i : ℕ), m (f i) (_ : P (f i))
msU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) ≤ ∑' (i : ℕ), m (f i) (_ : P (f i))
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
β : Type u_1
inst✝ : Countable β
f : β → Set α
hd : Pairwise (Disjoint on f)
hm : ∀ (i : β), P (f i)
⊢ extend m (⋃ (i : β), f i) = ∑' (i : β), extend m (f i)
cases nonempty_encodable β
case intro
α : Type u_2
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) = ∑' (i : ℕ), m (f i) (_ : P (f i))
msU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) ≤ ∑' (i : ℕ), m (f i) (_ : P (f i))
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
β : Type u_1
inst✝ : Countable β
f : β → Set α
hd : Pairwise (Disjoint on f)
hm : ∀ (i : β), P (f i)
val✝ : Encodable β
⊢ extend m (⋃ (i : ℕ) (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) =
    ∑' (i : ℕ), extend m (⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b)

case intro.m0
α : Type u_2
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) = ∑' (i : ℕ), m (f i) (_ : P (f i))
msU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) ≤ ∑' (i : ℕ), m (f i) (_ : P (f i))
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
β : Type u_1
inst✝ : Countable β
f : β → Set α
hd : Pairwise (Disjoint on f)
hm : ∀ (i : β), P (f i)
val✝ : Encodable β
⊢ extend m ∅ = 0
case intro
α : Type u_2
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) = ∑' (i : ℕ), m (f i) (_ : P (f i))
msU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) ≤ ∑' (i : ℕ), m (f i) (_ : P (f i))
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
β : Type u_1
inst✝ : Countable β
f : β → Set α
hd : Pairwise (Disjoint on f)
hm : ∀ (i : β), P (f i)
val✝ : Encodable β
⊢ extend m (⋃ (i : β), f i) = ∑' (i : β), extend m (f i)
rw [← Encodable.iUnion_decode₂, ← tsum_iUnion_decode₂]
no goals
case intro
α : Type u_2
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) = ∑' (i : ℕ), m (f i) (_ : P (f i))
msU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) ≤ ∑' (i : ℕ), m (f i) (_ : P (f i))
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
β : Type u_1
inst✝ : Countable β
f : β → Set α
hd : Pairwise (Disjoint on f)
hm : ∀ (i : β), P (f i)
val✝ : Encodable β
⊢ extend m (⋃ (i : ℕ) (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) =
    ∑' (i : ℕ), extend m (⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b)
exact
  extend_iUnion_nat PU (fun n => Encodable.iUnion_decode₂_cases P0 hm)
    (mU _ (Encodable.iUnion_decode₂_disjoint_on hd))
no goals
case intro.m0
α : Type u_2
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) = ∑' (i : ℕ), m (f i) (_ : P (f i))
msU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) ≤ ∑' (i : ℕ), m (f i) (_ : P (f i))
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
β : Type u_1
inst✝ : Countable β
f : β → Set α
hd : Pairwise (Disjoint on f)
hm : ∀ (i : β), P (f i)
val✝ : Encodable β
⊢ extend m ∅ = 0
exact extend_empty P0 m0