PrintForm Definitions finite sets Sections AutomataTheory Doc

At: one one sym 1 1 1 1

1. T: Type
2. S: Type
3. f: TS
4. g: ST
5. g o f = Id
6. f o g = Id

S ~ T

By: Unfold `one_one_corr` 0

Generated subgoal:

1 f:(ST), g:(TS). InvFuns(S; T; f; g)


About:
universefunctionequalexists