Kevin Lee (Jul 07 2023 at 16:14): 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: Nov 13 2025 at 04:27 UTC