PrintForm Definitions finite sets Sections AutomataTheory Doc

At: one one preser fin 1 1 1

1. T: Type
2. S: Type
3. n:
4. f: nT
5. Bij(n; T; f)
6. f1: TS
7. g: ST
8. InvFuns(T; S; f1; g)

n:, f:(nS). Bij(n; S; f)

By: Analyze 8

Generated subgoal:

18. g o f1 = Id
9. f1 o g = Id
n:, f:(nS). Bij(n; S; f)


About:
existsfunctionnatural_numberuniverse