PrintForm Definitions finite sets Sections AutomataTheory Doc

At: inv of fin is fin 1 1 2
1. T: Type
2. S: Type
3. f: TS
4. Fin(S)
5. s:S. Dec(t:T. f(t) = s)
6. EquivRel x,y:T. f(x) = f(y)

Fin(x,y:T//(f(x) = f(y)))
By: Inst Thm* Fin(T) & (T ~ S) Fin(S) [{s:S| t:T. f(t) = s };x,y:T//(f(x) = f(y))]
Generated subgoals:

1 Fin({s:S| t:T. f(t) = s })
2 {s:S| t:T. f(t) = s } ~ (x,y:T//(f(x) = f(y)))
37. Fin(x,y:T//(f(x) = f(y)))
Fin(x,y:T//(f(x) = f(y)))

About:
quotientequalapplysetexistsuniversefunctionall