α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
f : α → β
hs : Set.Infinite s
hf : MapsTo f s t
ht : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → f x ≠ f y
⊢ ¬Set.Finite t
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
f : α → β
hs : Set.Infinite s
hf : MapsTo f s t
ht : Set.Finite t
⊢ ∃ x, x ∈ s ∧ ∃ y, y ∈ s ∧ x ≠ y ∧ f x = f y
contrapose! ht
no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
f : α → β
hs : Set.Infinite s
hf : MapsTo f s t
ht : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → f x ≠ f y
⊢ ¬Set.Finite t
exact infinite_of_injOn_mapsTo (fun x hx y hy => not_imp_not.1 (ht x hx y hy)) hf hs