Nuprl - quot

Origin Definitions Sections StandardLIB Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
quot_1Nuprl Section: quot_1 - Support lemmas for quotient type.

Selected Objects
THM quotient_qinc E:(TTProp). (EquivRel x,y:T. E(x,y))  T  (x,y:T//E(x,y))

THM quot_elim E:(TTProp).
(EquivRel x,y:T. E(x,y))  (a,b:T. a = b  x,y:T//E(x,y)  E(a,b))

THM all_quot_elim E:(TTProp).
(EquivRel x,y:T. E(x,y))

(F:((x,y:T//E(x,y))Prop).
((w:x,y:T//E(x,y). SqStable(F(w)))
(
(((z:x,y:T//E(x,y). F(z))  (z:T. F(z))))

THM dec_iff_ex_bvfun E:(TTProp).
(x,y:T. Dec(E(x,y)))  (f:(TT). x,y:T. (x f y)  E(x,y))

THM decidable__quotient_equal E:(TTProp).
(EquivRel x,y:T. E(x,y))

(x,y:T. Dec(E(x,y)))  (u,v:x,y:T//E(x,y). Dec(u = v))

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Selected Objects
THM	quotient_qinc	E:(TTProp). (EquivRel x,y:T. E(x,y)) T (x,y:T//E(x,y))
THM	quot_elim	E:(TTProp). (EquivRel x,y:T. E(x,y)) (a,b:T. a = b x,y:T//E(x,y) E(a,b))
THM	all_quot_elim	E:(TTProp). (EquivRel x,y:T. E(x,y)) (F:((x,y:T//E(x,y))Prop). ((w:x,y:T//E(x,y). SqStable(F(w))) ( (((z:x,y:T//E(x,y). F(z)) (z:T. F(z))))
THM	dec_iff_ex_bvfun	E:(TTProp). (x,y:T. Dec(E(x,y))) (f:(TT). x,y:T. (x f y) E(x,y))
THM	decidable__quotient_equal	E:(TTProp). (EquivRel x,y:T. E(x,y)) (x,y:T. Dec(E(x,y))) (u,v:x,y:T//E(x,y). Dec(u = v))

Origin Definitions Sections StandardLIB Doc