α β : Type u
ι : Type v
f : ι → Cardinal
hf : BddAbove (range f)
⊢ sSup (range (lift ∘ f)) = sSup (range fun i => lift (f i))
α β : Type u
ι : Type v
f : ι → Cardinal
hf : BddAbove (range f)
⊢ lift (iSup f) = ⨆ (i : ι), lift (f i)
rw [iSup, iSup, lift_sSup hf, ← range_comp]
no goals
α β : Type u
ι : Type v
f : ι → Cardinal
hf : BddAbove (range f)
⊢ sSup (range (lift ∘ f)) = sSup (range fun i => lift (f i))
simp [Function.comp]