PrintForm Definitions finite sets Sections AutomataTheory Doc

At: inv of fin is fin 1

1. T: Type
2. S: Type
3. f: TS
4. Fin(S) & (s:S. Dec(t:T. f(t) = s))

Fin(x,y:T//(f(x) = f(y)))

By: Analyze 4

Generated subgoal:

14. Fin(S)
5. s:S. Dec(t:T. f(t) = s)
Fin(x,y:T//(f(x) = f(y)))


About:
quotientequalapplyuniversefunctionandallexists