R : Type ?u.772186
R' : Type ?u.772189
𝕜 : Type u_2
𝕜₂ : Type ?u.772195
𝕜₃ : Type ?u.772198
𝕝 : Type ?u.772201
E : Type u_3
E₂ : Type ?u.772207
E₃ : Type ?u.772210
F : Type ?u.772213
G : Type ?u.772216
ι✝ : Type ?u.772219
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ q : Seminorm 𝕜 E
x : E
ι : Type u_1
p : ι → Seminorm 𝕜 E
hp : BddAbove (range p)
⊢ (⨆ (p_1 : ↑(range p)), ↑↑p_1) = ⨆ (i : ι), ↑(p i)
R : Type ?u.772186
R' : Type ?u.772189
𝕜 : Type u_2
𝕜₂ : Type ?u.772195
𝕜₃ : Type ?u.772198
𝕝 : Type ?u.772201
E : Type u_3
E₂ : Type ?u.772207
E₃ : Type ?u.772210
F : Type ?u.772213
G : Type ?u.772216
ι✝ : Type ?u.772219
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ q : Seminorm 𝕜 E
x : E
ι : Type u_1
p : ι → Seminorm 𝕜 E
hp : BddAbove (range p)
⊢ ↑(⨆ (i : ι), p i) = ⨆ (i : ι), ↑(p i)
rw [← sSup_range, Seminorm.coe_sSup_eq hp]
no goals
R : Type ?u.772186
R' : Type ?u.772189
𝕜 : Type u_2
𝕜₂ : Type ?u.772195
𝕜₃ : Type ?u.772198
𝕝 : Type ?u.772201
E : Type u_3
E₂ : Type ?u.772207
E₃ : Type ?u.772210
F : Type ?u.772213
G : Type ?u.772216
ι✝ : Type ?u.772219
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ q : Seminorm 𝕜 E
x : E
ι : Type u_1
p : ι → Seminorm 𝕜 E
hp : BddAbove (range p)
⊢ (⨆ (p_1 : ↑(range p)), ↑↑p_1) = ⨆ (i : ι), ↑(p i)
exact iSup_range' (fun p : Seminorm 𝕜 E => (p : E → ℝ)) p