PrintForm Definitions finite sets Sections AutomataTheory Doc

At: prod fin is fin 1 2 3

1. T: Type
2. t: T
3. n:
4. f: nT
5. Bij(n; T; f)
6. n > 0
7. x: (nn)

(x n) < n

By: BackThru Thm* n:, x:(nn). (x n) < n

Generated subgoals:

None


About:
less_thandivideuniversefunctionnatural_numbermultiply