PrintForm Definitions finite sets Sections AutomataTheory Doc

At: one one preser fin 1 1 1 1 1 1 1 1 1 1 1 1 1 1
1. T: Type
2. S: Type
3. n:
4. f: nT
5. Inj(n; T; f)
6. Surj(n; T; f)
7. f1: TS
8. g: ST
9. g o f1 = Id
10. f1 o g = Id
11. a1: n
12. a2: n
13. (f1 o f)(a1) = (f1 o f)(a2)
14. f(a1) = f(a2)

a1 = a2
By: Unfold `inject` 5
Generated subgoal:

15. a1,a2:n. f(a1) = f(a2) a1 = a2
6. Surj(n; T; f)
7. f1: TS
8. g: ST
9. g o f1 = Id
10. f1 o g = Id
11. a1: n
12. a2: n
13. (f1 o f)(a1) = (f1 o f)(a2)
14. f(a1) = f(a2)
a1 = a2

About:
equalnatural_numberuniversefunctionapply