Selected Objects

THM	not_dec_is_dec	P:(AProp). (x:A. P(x) P(x)) & (x:A. P(x)) (x:A. P(x)) (x:A. P(x)) (x:A. P(x))
THM	rect_enumer	n,m:. f:(nm(nm)). Bij(nm; (nm); f)
def	finite	Fin(s) == n:, f:(ns). Bij(n; s; f)
THM	nsub_is_finite	n:. Fin(n)
THM	bool_is_finite	Fin()
THM	one2one_preserves_fin	(T ~ U) & Fin(T) Fin(U)
THM	fin_iff_1_1_nsub	Fin(T) (m:. m ~ T)
THM	div_bounds_2	n:, x:(nn). (x n) < n
THM	prod_fin_is_fin	t:T. Fin(T) Fin(TT)
THM	fin_dec_fin	n:, T:Type, B:(TProp). (n ~ T) & (t:T. Dec(B(t))) (m:. m ~ {t:T| B(t) })
THM	finite_decidable_subset	B:(TProp). Fin(T) & (t:T. Dec(B(t))) Fin({t:T| B(t) })
THM	one_one_preser_fin	Fin(T) & (T ~ S) Fin(S)
THM	set_function	R:(STProp). (s:S. Dec(t:T. R(s,t))) (f:({s:S| t:T. R(s,t) }T). s:{s:S| t:T. R(s,t) }. R(s,f(s)))
THM	inv_of_fin_is_fin	f:(TS). Fin(S) & (s:S. Dec(t:T. f(t) = s)) Fin(x,y:T//(f(x) = f(y)))
THM	fin_is_decid	Fin(T) (x,y:T. Dec(x = y))
THM	fin_dist_func	Fin(St) (eq:(StSt). x,y:St. eq(x,y) x = y)
THM	decid_is_comp	f:(TProp). (t:T. Dec(f(t))) (g:(T). t:T. f(t) g(t))
THM	auto2_list_ind	P:(Alph*Prop). (n:. (l:Alph*. ||l|| < n P(l)) (l:Alph*. ||l|| = n P(l))) (l:Alph*. P(l))
THM	one_one_sym	(T ~ S) (S ~ T)
COM	phole_descr	Pigeon-hole principle
THM	phole_aux	n:{1...}, f:((n+1)n). i:(n+1), j:i. f(i) = f(j)
THM	phole_lemma	n:{1...}, m:{n+1...}, f:(mn). i,j:m. i < j & f(i) = f(j)
def	card	#(t)=n == t ~ n