Selected Objects

THM	incl_aux2_quo	n:{1...}, m:n, E:(nnProp). (EquivRel x,y:n. x E y) (z:x,y:m//(x E y). z x,y:n//(x E y))
THM	incl_aux3_quo	n:{1...}, m:n, E:(nnProp). (EquivRel i,j:n. i E j) (x,y:i,j:m//(i E j). x = y i,j:n//(i E j) x = y)
THM	incl_aux4_quo	n:{1...}, E:(nnProp). (EquivRel i,j:n. i E j) (x:i,j:n//(i E j). x = n-1 i,j:n//(i E j) x i,j:(n-1)//(i E j))
THM	incl_aux5_quo	E:(TTProp). (EquivRel x,y:T. x E y) (x,y:T. x = y x = y u,v:T//(u E v))
THM	incl_aux6_quo	R:(TTProp). (EquivRel x,y:T. x R y) (Q:((x,y:T//(x R y))(x,y:T//(x R y))Prop). (EquivRel u,v:x,y:T//(x R y). u Q v) (EquivRel x,y:T. x Q y))
THM	rest_refl_rel	n:{1...}, m:n, E:(nnProp). Refl(n;x,y.x E y) Refl(m;x,y.x E y)
THM	rest_symm_rel	n:{1...}, m:n, E:(nnProp). Sym x,y:n. x E y Sym x,y:m. x E y
THM	rest_tran_rel	n:{1...}, m:n, E:(nnProp). Trans x,y:n. x E y Trans x,y:m. x E y
THM	rest_equi_rel	n:{1...}, m:n, E:(nnProp). (EquivRel x,y:n. x E y) (EquivRel x,y:m. x E y)
THM	quotient_of_nsubn	n:{1...}, E:(nnProp). (EquivRel x,y:n. x E y) & (x,y:n. Dec(x E y)) (m:(n+1). m ~ (i,j:n//(i E j)))
THM	quo_of_quo	R:(TTProp). (EquivRel x,y:T. x R y) (Q:((x,y:T//(x R y))(x,y:T//(x R y))Prop). (EquivRel u,v:x,y:T//(x R y). u Q v) ((x,y:T//(x Q y)) ~ (u,v:(x,y:T//(x R y))//(u Q v))))
def	preima_of_rel	R_f(x,y) == (f(x)) R (f(y))
THM	preima_of_equiv_rel	f:(AB), R:(BBProp). (EquivRel x,y:B. x R y) (EquivRel x,y:A. x R_f y)
THM	one_one_corr_refl	A ~ A
THM	one_one_corr_symm	(A ~ B) (B ~ A)
THM	one_one_corr_tran	(A ~ B) (B ~ C) (A ~ C)
THM	quotient_1_1_corr	f:(AB), R:(BBProp). Bij(A; B; f) (EquivRel x,y:B. x R y) (F:((x,y:A//(x R_f y))(x,y:B//(x R y))). Bij(x,y:A//(x R_f y); x,y:B//(x R y); F))
THM	quotient_of_finite	n:{1...}, A:Type, R:(AAProp). (n ~ A) (EquivRel x,y:A. x R y) (x,y:A. Dec(x R y)) (m:(n+1). m ~ (x,y:A//(x R y)))