α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : Infinite α
f : α → β
hi : Injective f
⊢ Set.Infinite univ
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : Infinite α
f : α → β
hi : Injective f
⊢ Set.Infinite (range f)
rw [← image_univ, infinite_image_iff (injOn_of_injective hi _)]
no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : Infinite α
f : α → β
hi : Injective f
⊢ Set.Infinite univ
exact infinite_univ