α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hs : Set.Countable s
f : α → β
⊢ Set.Countable (range fun x => f ↑x)
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hs : Set.Countable s
f : α → β
⊢ Set.Countable (f '' s)
rw [image_eq_range]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hs : Set.Countable s
f : α → β
this : Countable ↑s
⊢ Set.Countable (range fun x => f ↑x)
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hs : Set.Countable s
f : α → β
⊢ Set.Countable (range fun x => f ↑x)
haveI := hs.to_subtype
no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hs : Set.Countable s
f : α → β
this : Countable ↑s
⊢ Set.Countable (range fun x => f ↑x)
apply countable_range