PrintForm Definitions finite sets Sections AutomataTheory Doc

At: prod fin is fin 1 2 6 1
1. T: Type
2. t: T
3. n:
4. f: nT
5. Inj(n; T; f)
6. Surj(n; T; f)
7. n > 0

Inj((nn); TT; x. < f(x n),f(x rem n) > )
By:
Unfold `inject` 0
THEN
Unfold `inject` 5
Generated subgoal:

15. a1,a2:n. f(a1) = f(a2) a1 = a2
6. Surj(n; T; f)
7. n > 0
a1,a2:(nn). (x. < f(x n),f(x rem n) > )(a1) = (x. < f(x n),f(x rem n) > )(a2) TT a1 = a2

About:
natural_numbermultiplyproductlambdapairapplydivide
remainderuniversefunctionallimpliesequal