Functions between sets

Stream: new members

[Dan Stanescu]

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]

You're fighting type theory really hard here.

[Reid Barton]

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]

The nonempty hypotheses are unnecessary

[Dan Stanescu]

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