Stream: Beginner Questions

Topic: Injectivity + finite equal sized sets implies surjectivity

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

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

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