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?

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.

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: Feb 27 2024 at 08:17 UTC