PrintForm Definitions finite sets Sections AutomataTheory Doc

At: one one preser fin 1 1 1 1 1 1 2 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. b: S

a:n. (f1 o f)(a) = b
By: Unfold `surject` 6
Generated subgoal:

16. b:T. a:n. f(a) = b
7. f1: TS
8. g: ST
9. g o f1 = Id
10. f1 o g = Id
11. b: S
a:n. (f1 o f)(a) = b

About:
existsnatural_numberequalapplyuniversefunction