## Stream: new members

### Topic: Functions between sets

#### Dan Stanescu (Jul 04 2020 at 13:33):

I want to prove this in a way that is easy to follow for someone taking a first class in analysis. In my mind, that means showing the intermediary goals in the sketch proof below. This doesn't compile because of coercion problems and I'm not sure how to make it work while still keeping a very explicit statement of what is intended. Help will be greatly appreciated.

import data.set.basic
import data.real.basic
import topology.basic

open set
open function

lemma finite_of_inj (A B : set ℝ) (hA : A.nonempty) (h1B : B.nonempty) (h2B : finite B)
(H : ∃ (f : A → B), injective f) : finite A :=
begin
cases H with f hf,
have h1 : set.image f A ⊆ B, {sorry}, --does not compile
have h2 : ∃ g : A → set.image f A, bijective g, {sorry}, -- bijective version of f
have h3 : finite (set.image f A), {sorry}, -- from h1
sorry, -- goal should follow from h2, h3
end


#### Patrick Massot (Jul 04 2020 at 13:41):

You're fighting type theory really hard here.

#### Reid Barton (Jul 04 2020 at 13:52):

If you want to prove this statement here is a better way to get started

import data.set.basic
import data.real.basic
import topology.basic

open set
open function

lemma finite_of_inj (A B : set ℝ) (hA : A.nonempty) (h1B : B.nonempty) (h2B : finite B)
(H : ∃ (f : A → B), injective f) : finite A :=
begin
cases H with f hf,
let g := range_factorization f,
have h2 : bijective g := ⟨subtype.coind_injective _ hf, surjective_onto_range⟩,
have h3 : finite (range f), {sorry},
sorry, -- goal should follow from h2, h3
end


#### Reid Barton (Jul 04 2020 at 13:52):

The nonempty hypotheses are unnecessary

#### Dan Stanescu (Jul 04 2020 at 17:25):

Thanks @Reid Barton
Even starting as you indicate, h3 is still difficult to get. In the end I settled on the following, which I post here for completeness.

import data.set.basic
import data.real.basic
import topology.basic

open set
open function

variables (α β : Type) [fintype β]

lemma finite_of_inj  (A : set α) (H : ∃ (f : α → β), inj_on f A) : finite A :=
begin
cases H with f hf,
have h0 := finite.of_fintype (set.image f A),
exact finite_of_finite_image hf h0,
end


Last updated: May 08 2021 at 18:17 UTC