α : Type u_2
β : Type u_1
γ : Type ?u.376229
δ : Type u_3
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 : δ → β
t : Finset δ
⊢ R (m (⨆ (x : { d // d ∈ t }), s ↑x)) (∑' (x : { x // x ∈ t }), m (s ↑x))
α : Type u_2
β : Type u_1
γ : Type ?u.376229
δ : Type u_3
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 : δ → β
t : Finset δ
⊢ R (m (⨆ (d : δ) (_ : d ∈ t), s d)) (∑ d in t, m (s d))
rw [iSup_subtype', ← Finset.tsum_subtype]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.376229
δ : Type u_3
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 : δ → β
t : Finset δ
⊢ R (m (⨆ (x : { d // d ∈ t }), s ↑x)) (∑' (x : { x // x ∈ t }), m (s ↑x))
exact rel_iSup_tsum m m0 R m_iSup _