PrintForm Definitions automata 5 Sections AutomataTheory Doc

At: surj is inj gen

A,B:Type, f:(AB). (A ~ B) & Fin(B) Surj(A; B; f) Inj(A; B; f)
By:
Unfold `one_one_corr` 0
THEN
Unfold `finite` 0
THEN
UnivCD
Generated subgoal:

11. A: Type
2. B: Type
3. f: AB
4. (f:(AB), g:(BA). InvFuns(A; B; f; g)) & (n:, f:(nB). Bij(n; B; f))
5. Surj(A; B; f)
Inj(A; B; f)

About:
alluniversefunctionimpliesand