Zulip Chat Archive

Stream: new members

Topic: Functions between sets


view this post on Zulip 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

view this post on Zulip Patrick Massot (Jul 04 2020 at 13:41):

You're fighting type theory really hard here.

view this post on Zulip 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

view this post on Zulip Reid Barton (Jul 04 2020 at 13:52):

The nonempty hypotheses are unnecessary

view this post on Zulip 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