PrintForm Definitions finite sets Sections AutomataTheory Doc

At: inv of fin is fin 1 1 2 1

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({s:S| t:T. f(t) = s })

By: Inst Thm* B:(TProp). Fin(T) & (t:T. Dec(B(t))) Fin({t:T| B(t) }) [S;s.t:T. f(t) = s]

Generated subgoals:

17. t: S
Dec((s.t:T. f(t) = s)(t))
27. Fin({t:S| (s.t:T. f(t) = s)(t) })
Fin({s:S| t:T. f(t) = s })


About:
setexistsequalapplylambdauniversefunctionall