α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
t : Set β
hs : Set.Countable s
ht : Set.Countable t
f : α → β → γ
⊢ Set.Countable ((fun x => f x.fst x.snd) '' s ×ˢ t)
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
t : Set β
hs : Set.Countable s
ht : Set.Countable t
f : α → β → γ
⊢ Set.Countable (Set.image2 f s t)
rw [← image_prod]
no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
t : Set β
hs : Set.Countable s
ht : Set.Countable t
f : α → β → γ
⊢ Set.Countable ((fun x => f x.fst x.snd) '' s ×ˢ t)
exact (hs.prod ht).image _