α β : Type u
f : Cardinal → Cardinal
s : Set Cardinal
hs : Small ↑s
⊢ Small ↑(f '' s)
α β : Type u
f : Cardinal → Cardinal
s : Set Cardinal
hs : BddAbove s
⊢ BddAbove (f '' s)
rw [bddAbove_iff_small] at hs ⊢
no goals
α β : Type u
f : Cardinal → Cardinal
s : Set Cardinal
hs : Small ↑s
⊢ Small ↑(f '' s)
exact small_lift.{_,v,_} _