Entry	Value
Package Name	set-finite-def
Count	5
Theorems	FINITE_CASES : !a. FINITE a <=> a = {} \/ (?x s. a = x INSERT s /\ FINITE s) FINITE_EMPTY : FINITE {} FINITE_INDUCT : !p. p {} /\ (!x s. p s ==> p (x INSERT s)) ==> (!a. FINITE a ==> p a) FINITE_INSERT_IMP : !x s. FINITE s ==> FINITE (x INSERT s) INFINITE : !s. INFINITE s <=> ~FINITE s

Back to main package page