α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β
s : Set α
h_inf : Set.Infinite s
h_fin : Set.Finite (f '' s)
this : Finite ↑(f '' s)
⊢ ¬InjOn f s
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β
s : Set α
h_inf : Set.Infinite s
h_fin : Set.Finite (f '' s)
⊢ ¬InjOn f s
have : Finite (f '' s) := finite_coe_iff.mpr h_fin
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β
s : Set α
h_inf : Set.Infinite s
h_fin : Set.Finite (f '' s)
this✝ : Finite ↑(f '' s)
this : Infinite ↑s
⊢ ¬InjOn f s
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β
s : Set α
h_inf : Set.Infinite s
h_fin : Set.Finite (f '' s)
this : Finite ↑(f '' s)
⊢ ¬InjOn f s
have : Infinite s := infinite_coe_iff.mpr h_inf
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β
s : Set α
h_inf : Set.Infinite s
h_fin : Set.Finite (f '' s)
this✝ : Finite ↑(f '' s)
this : Infinite ↑s
h : ¬Injective (codRestrict (restrict s f) (f '' s) (_ : ∀ (x : ↑s), ∃ a, a ∈ s ∧ f a = restrict s f x))
⊢ ¬InjOn f s
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β
s : Set α
h_inf : Set.Infinite s
h_fin : Set.Finite (f '' s)
this✝ : Finite ↑(f '' s)
this : Infinite ↑s
⊢ ¬InjOn f s
have h := not_injective_infinite_finite
          ((f '' s).codRestrict (s.restrict f) fun x => ⟨x, x.property, rfl⟩)
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β
s : Set α
h_inf : Set.Infinite s
h_fin : Set.Finite (f '' s)
this✝ : Finite ↑(f '' s)
this : Infinite ↑s
h : ¬¬InjOn f s
⊢ Injective (codRestrict (restrict s f) (f '' s) (_ : ∀ (x : ↑s), ∃ a, a ∈ s ∧ f a = restrict s f x))
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β
s : Set α
h_inf : Set.Infinite s
h_fin : Set.Finite (f '' s)
this✝ : Finite ↑(f '' s)
this : Infinite ↑s
h : ¬Injective (codRestrict (restrict s f) (f '' s) (_ : ∀ (x : ↑s), ∃ a, a ∈ s ∧ f a = restrict s f x))
⊢ ¬InjOn f s
contrapose! h
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β
s : Set α
h_inf : Set.Infinite s
h_fin : Set.Finite (f '' s)
this✝ : Finite ↑(f '' s)
this : Infinite ↑s
h : ¬¬InjOn f s
⊢ InjOn f s
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β
s : Set α
h_inf : Set.Infinite s
h_fin : Set.Finite (f '' s)
this✝ : Finite ↑(f '' s)
this : Infinite ↑s
h : ¬¬InjOn f s
⊢ Injective (codRestrict (restrict s f) (f '' s) (_ : ∀ (x : ↑s), ∃ a, a ∈ s ∧ f a = restrict s f x))
rw [injective_codRestrict, ← injOn_iff_injective]
no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β
s : Set α
h_inf : Set.Infinite s
h_fin : Set.Finite (f '' s)
this✝ : Finite ↑(f '' s)
this : Infinite ↑s
h : ¬¬InjOn f s
⊢ InjOn f s
rwa [not_not] at h