case intro
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
⊢ HasSum (fun i => ↑v (f i)) (↑v (⋃ (i : β), f i))
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ HasSum (fun i => ↑v (f i)) (↑v (⋃ (i : β), f i))
cases nonempty_encodable β
case intro
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
⊢ HasSum (fun i => ↑v (f i)) (↑v (⋃ (i : β), f i))
case intro
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
⊢ HasSum (fun i => ↑v (f i)) (↑v (⋃ (i : β), f i))
set g := fun i : ℕ => ⋃ (b : β) (H : b ∈ Encodable.decode₂ β i), f b with hg
case intro
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
⊢ HasSum (fun i => ↑v (f i)) (↑v (⋃ (i : β), f i))
case intro
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
⊢ HasSum (fun i => ↑v (f i)) (↑v (⋃ (i : β), f i))
have hg₁ : ∀ i, MeasurableSet (g i) :=
  fun _ => MeasurableSet.iUnion fun b => MeasurableSet.iUnion fun _ => hf₁ b
case intro
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
⊢ HasSum (fun i => ↑v (f i)) (↑v (⋃ (i : β), f i))
case intro
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
⊢ HasSum (fun i => ↑v (f i)) (↑v (⋃ (i : β), f i))
have hg₂ : Pairwise (Disjoint on g) := Encodable.iUnion_decode₂_disjoint_on hf₂
case intro
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (i : ℕ), g i) = ∑' (i : ℕ), ↑v (g i)
⊢ HasSum (fun i => ↑v (f i)) (↑v (⋃ (i : β), f i))
case intro
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
⊢ HasSum (fun i => ↑v (f i)) (↑v (⋃ (i : β), f i))
have := v.of_disjoint_iUnion_nat hg₁ hg₂
case intro
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
⊢ HasSum (fun i => ↑v (f i)) (↑v (⋃ (i : β), f i))
case intro
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (i : ℕ), g i) = ∑' (i : ℕ), ↑v (g i)
⊢ HasSum (fun i => ↑v (f i)) (↑v (⋃ (i : β), f i))
rw [hg, Encodable.iUnion_decode₂] at this
case intro.m0
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
hg₃ : (fun i => ↑v (f i)) = fun i => ↑v (g (Encodable.encode i))
⊢ ↑v ∅ = 0

case intro
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
hg₃ : (fun i => ↑v (f i)) = fun i => ↑v (g (Encodable.encode i))
⊢ Summable fun i => ↑v (f i)
case intro
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
hg₃ : (fun i => ↑v (f i)) = fun i => ↑v (g (Encodable.encode i))
⊢ HasSum (fun i => ↑v (f i)) (↑v (⋃ (i : β), f i))
rw [Summable.hasSum_iff, this, ← tsum_iUnion_decode₂]
case h
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
x : β
⊢ ↑v (f x) = ↑v (g (Encodable.encode x))
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
⊢ (fun i => ↑v (f i)) = fun i => ↑v (g (Encodable.encode i))
ext x
case h
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
x : β
⊢ ↑v (f x) = ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) (Encodable.encode x))
case h
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
x : β
⊢ ↑v (f x) = ↑v (g (Encodable.encode x))
rw [hg]
case h
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
x : β
⊢ ↑v (f x) = ↑v (⋃ (b : β) (_ : b ∈ Encodable.decode₂ β (Encodable.encode x)), f b)
case h
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
x : β
⊢ ↑v (f x) = ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) (Encodable.encode x))
simp only
case h.e_a
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
x : β
⊢ f x = ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β (Encodable.encode x)), f b
case h
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
x : β
⊢ ↑v (f x) = ↑v (⋃ (b : β) (_ : b ∈ Encodable.decode₂ β (Encodable.encode x)), f b)
congr
case h.e_a.h
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
x : β
y : α
⊢ y ∈ f x ↔ y ∈ ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β (Encodable.encode x)), f b
case h.e_a
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
x : β
⊢ f x = ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β (Encodable.encode x)), f b
ext y
case h.e_a.h
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
x : β
y : α
⊢ y ∈ f x ↔ ∃ i, Encodable.decode₂ β (Encodable.encode x) = Option.some i ∧ y ∈ f i
case h.e_a.h
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
x : β
y : α
⊢ y ∈ f x ↔ y ∈ ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β (Encodable.encode x)), f b
simp only [exists_prop, Set.mem_iUnion, Option.mem_def]
case h.e_a.h.mp
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
x : β
y : α
⊢ y ∈ f x → ∃ i, Encodable.decode₂ β (Encodable.encode x) = Option.some i ∧ y ∈ f i

case h.e_a.h.mpr
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
x : β
y : α
⊢ (∃ i, Encodable.decode₂ β (Encodable.encode x) = Option.some i ∧ y ∈ f i) → y ∈ f x
case h.e_a.h
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
x : β
y : α
⊢ y ∈ f x ↔ ∃ i, Encodable.decode₂ β (Encodable.encode x) = Option.some i ∧ y ∈ f i
constructor
case h.e_a.h.mp
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
x : β
y : α
hy : y ∈ f x
⊢ ∃ i, Encodable.decode₂ β (Encodable.encode x) = Option.some i ∧ y ∈ f i
case h.e_a.h.mp
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
x : β
y : α
⊢ y ∈ f x → ∃ i, Encodable.decode₂ β (Encodable.encode x) = Option.some i ∧ y ∈ f i
intro hy
no goals
case h.e_a.h.mp
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
x : β
y : α
hy : y ∈ f x
⊢ ∃ i, Encodable.decode₂ β (Encodable.encode x) = Option.some i ∧ y ∈ f i
refine' ⟨x, (Encodable.decode₂_is_partial_inv _ _).2 rfl, hy⟩
case h.e_a.h.mpr.intro.intro
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
x : β
y : α
b : β
hb₁ : Encodable.decode₂ β (Encodable.encode x) = Option.some b
hb₂ : y ∈ f b
⊢ y ∈ f x
case h.e_a.h.mpr
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
x : β
y : α
⊢ (∃ i, Encodable.decode₂ β (Encodable.encode x) = Option.some i ∧ y ∈ f i) → y ∈ f x
rintro ⟨b, hb₁, hb₂⟩
case h.e_a.h.mpr.intro.intro
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
x : β
y : α
b : β
hb₁ : Encodable.encode b = Encodable.encode x
hb₂ : y ∈ f b
⊢ y ∈ f x
case h.e_a.h.mpr.intro.intro
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
x : β
y : α
b : β
hb₁ : Encodable.decode₂ β (Encodable.encode x) = Option.some b
hb₂ : y ∈ f b
⊢ y ∈ f x
rw [Encodable.decode₂_is_partial_inv _ _] at hb₁
no goals
case h.e_a.h.mpr.intro.intro
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
x : β
y : α
b : β
hb₁ : Encodable.encode b = Encodable.encode x
hb₂ : y ∈ f b
⊢ y ∈ f x
rwa [← Encodable.encode_injective hb₁]
no goals
case intro.m0
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
hg₃ : (fun i => ↑v (f i)) = fun i => ↑v (g (Encodable.encode i))
⊢ ↑v ∅ = 0
exact v.empty
case intro
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
hg₃ : (fun i => ↑v (f i)) = fun i => ↑v (g (Encodable.encode i))
⊢ Summable fun i => ↑v (g (Encodable.encode i))
case intro
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
hg₃ : (fun i => ↑v (f i)) = fun i => ↑v (g (Encodable.encode i))
⊢ Summable fun i => ↑v (f i)
rw [hg₃]
case intro
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
hg₃ : (fun i => ↑v (f i)) = fun i => ↑v (g (Encodable.encode i))
⊢ Summable ((fun i => ↑v (g i)) ∘ Encodable.encode)
case intro
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
hg₃ : (fun i => ↑v (f i)) = fun i => ↑v (g (Encodable.encode i))
⊢ Summable fun i => ↑v (g (Encodable.encode i))
change Summable ((fun i => v (g i)) ∘ Encodable.encode)
case intro
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
hg₃ : (fun i => ↑v (f i)) = fun i => ↑v (g (Encodable.encode i))
⊢ Summable fun i => ↑v (g i)

case intro
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
hg₃ : (fun i => ↑v (f i)) = fun i => ↑v (g (Encodable.encode i))
⊢ ∀ (x : ℕ), ¬x ∈ Set.range Encodable.encode → ↑v (g x) = 0
case intro
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
hg₃ : (fun i => ↑v (f i)) = fun i => ↑v (g (Encodable.encode i))
⊢ Summable ((fun i => ↑v (g i)) ∘ Encodable.encode)
rw [Function.Injective.summable_iff Encodable.encode_injective]
no goals
case intro
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
hg₃ : (fun i => ↑v (f i)) = fun i => ↑v (g (Encodable.encode i))
⊢ Summable fun i => ↑v (g i)
exact (v.m_iUnion hg₁ hg₂).summable
case intro
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
hg₃ : (fun i => ↑v (f i)) = fun i => ↑v (g (Encodable.encode i))
x : ℕ
hx : ¬x ∈ Set.range Encodable.encode
⊢ ↑v (g x) = 0
case intro
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
hg₃ : (fun i => ↑v (f i)) = fun i => ↑v (g (Encodable.encode i))
⊢ ∀ (x : ℕ), ¬x ∈ Set.range Encodable.encode → ↑v (g x) = 0
intro x hx
case h.e'_2.h.e'_7
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
hg₃ : (fun i => ↑v (f i)) = fun i => ↑v (g (Encodable.encode i))
x : ℕ
hx : ¬x ∈ Set.range Encodable.encode
⊢ g x = ∅
case intro
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
hg₃ : (fun i => ↑v (f i)) = fun i => ↑v (g (Encodable.encode i))
x : ℕ
hx : ¬x ∈ Set.range Encodable.encode
⊢ ↑v (g x) = 0
convert v.empty
case h.e'_2.h.e'_7
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
hg₃ : (fun i => ↑v (f i)) = fun i => ↑v (g (Encodable.encode i))
x : ℕ
hx : ∀ (x_1 : β), ¬Encodable.encode x_1 = x
⊢ ∀ (i : β), Encodable.decode₂ β x = Option.some i → f i = ∅
case h.e'_2.h.e'_7
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
hg₃ : (fun i => ↑v (f i)) = fun i => ↑v (g (Encodable.encode i))
x : ℕ
hx : ¬x ∈ Set.range Encodable.encode
⊢ g x = ∅
simp only [Set.iUnion_eq_empty, Option.mem_def, not_exists, Set.mem_range] at hx⊢
case h.e'_2.h.e'_7
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
hg₃ : (fun i => ↑v (f i)) = fun i => ↑v (g (Encodable.encode i))
x : ℕ
hx : ∀ (x_1 : β), ¬Encodable.encode x_1 = x
i : β
hi : Encodable.decode₂ β x = Option.some i
⊢ f i = ∅
case h.e'_2.h.e'_7
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
hg₃ : (fun i => ↑v (f i)) = fun i => ↑v (g (Encodable.encode i))
x : ℕ
hx : ∀ (x_1 : β), ¬Encodable.encode x_1 = x
⊢ ∀ (i : β), Encodable.decode₂ β x = Option.some i → f i = ∅
intro i hi
no goals
case h.e'_2.h.e'_7
α : Type u_2
β : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
hg₃ : (fun i => ↑v (f i)) = fun i => ↑v (g (Encodable.encode i))
x : ℕ
hx : ∀ (x_1 : β), ¬Encodable.encode x_1 = x
i : β
hi : Encodable.decode₂ β x = Option.some i
⊢ f i = ∅
exact False.elim ((hx i) ((Encodable.decode₂_is_partial_inv _ _).1 hi))