## Stream: Beginner Questions

### Topic: Injectivity + finite equal sized sets implies surjectivity

#### Kevin Lee (Jul 07 2023 at 16:14):

I have defined a function `g :: "nat => int"` and showed these two statements:
`"∀i ∈ {0..m-1}. ∀j ∈ {0..m-1}. g i = g j ⟶ i = j"` and
`"∀ i ∈ {0..m-1}. g i ∈ {0..m-1}"`.

How can I show surjectivity? Is there something in the function libraries that can help?

#### Wolfgang Jeltsch (Jul 07 2023 at 16:44):

I guess you’re making again the mistake of using HOL constructs where Pure (meta-logic) constructs exist. If you use the latter, things might become much simpler. For the first statement, perhaps applying an introduction rule for surjectivity (which should be called `surjI`) will be enough.

#### Yong Kiam (Jul 08 2023 at 14:47):

in addition the above, you could use Finite_Set.surjective_iff_injective_gen

(the way I found this lemma was to search using the patterns "inj_on" and "card _ = card _")

you could also consider writing the ranges as {0..<m}

Last updated: Dec 07 2023 at 20:16 UTC