α : Type u_1
β : Type ?u.5450
γ : Type ?u.5453
ι : Sort u_2
inst✝¹ : Preorder α
inst✝ : SupSet α
f : ι → α
h : BddAbove (range f)
⊢ sSup (range ((fun a => ↑a) ∘ f)) = sSup (range fun i => ↑(f i))
α : Type u_1
β : Type ?u.5450
γ : Type ?u.5453
ι : Sort u_2
inst✝¹ : Preorder α
inst✝ : SupSet α
f : ι → α
h : BddAbove (range f)
⊢ ↑(⨆ (i : ι), f i) = ⨆ (i : ι), ↑(f i)
rw [iSup, iSup, WithTop.coe_sSup' h, ← range_comp]
no goals
α : Type u_1
β : Type ?u.5450
γ : Type ?u.5453
ι : Sort u_2
inst✝¹ : Preorder α
inst✝ : SupSet α
f : ι → α
h : BddAbove (range f)
⊢ sSup (range ((fun a => ↑a) ∘ f)) = sSup (range fun i => ↑(f i))
rfl