PrintForm Definitions finite sets Sections AutomataTheory Doc

At: one2one preserves fin 1 1 1 1 1 1 1 1 1 1 1 1 1
1. T: Type
2. U: Type
3. f: TU
4. g: UT
5. g o f = Id
6. f o g = Id
7. n:
8. f1: nT
9. Inj(n; T; f1)
10. Surj(n; T; f1)

Inj(n; U; f o f1) & Surj(n; U; f o f1)
By: Analyze 0
Generated subgoals:

1 Inj(n; U; f o f1)
2 Surj(n; U; f o f1)

About:
andnatural_numberuniversefunctionequal