case intro
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.374689
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Countable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
R : α → α → Prop
m_iSup : ∀ (s : ℕ → β), R (m (⨆ (i : ℕ), s i)) (∑' (i : ℕ), m (s i))
s : γ → β
val✝ : Encodable γ
⊢ R (m (⨆ (b : γ), s b)) (∑' (b : γ), m (s b))
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.374689
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Countable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
R : α → α → Prop
m_iSup : ∀ (s : ℕ → β), R (m (⨆ (i : ℕ), s i)) (∑' (i : ℕ), m (s i))
s : γ → β
⊢ R (m (⨆ (b : γ), s b)) (∑' (b : γ), m (s b))
cases nonempty_encodable γ
case intro
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.374689
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Countable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
R : α → α → Prop
m_iSup : ∀ (s : ℕ → β), R (m (⨆ (i : ℕ), s i)) (∑' (i : ℕ), m (s i))
s : γ → β
val✝ : Encodable γ
⊢ R (m (⨆ (i : ℕ) (b : γ) (_ : b ∈ decode₂ γ i), s b)) (∑' (i : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b))
case intro
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.374689
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Countable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
R : α → α → Prop
m_iSup : ∀ (s : ℕ → β), R (m (⨆ (i : ℕ), s i)) (∑' (i : ℕ), m (s i))
s : γ → β
val✝ : Encodable γ
⊢ R (m (⨆ (b : γ), s b)) (∑' (b : γ), m (s b))
rw [← iSup_decode₂, ← tsum_iSup_decode₂ _ m0 s]
no goals
case intro
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.374689
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Countable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
R : α → α → Prop
m_iSup : ∀ (s : ℕ → β), R (m (⨆ (i : ℕ), s i)) (∑' (i : ℕ), m (s i))
s : γ → β
val✝ : Encodable γ
⊢ R (m (⨆ (i : ℕ) (b : γ) (_ : b ∈ decode₂ γ i), s b)) (∑' (i : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b))
exact m_iSup _