is mentioned by
![]() ![]() ![]() ![]() ![]() Thm* ( ![]() Thm* ![]() ![]() Thm* Linorder(T;x,y.R(x,y)) ![]() ![]() ![]() ![]() ![]() ![]() | [linorder_lt_neg] |
![]() ![]() ![]() ![]() ![]() Thm* Linorder(T;x,y.R(x,y)) ![]() ![]() ![]() ![]() ![]() ![]() | [linorder_le_neg] |
![]() ![]() ![]() ![]() ![]() Thm* (Trans a,b:T. R(a,b)) Thm* ![]() ![]() Thm* ( ![]() Thm* (strict_part(x,y.R(x,y);a;b) ![]() ![]() ![]() ![]() | [trans_imp_sp_trans_b] |
![]() ![]() ![]() ![]() ![]() Thm* (Trans a,b:T. R(a,b)) Thm* ![]() ![]() Thm* ( ![]() Thm* (R(a,b) ![]() ![]() ![]() ![]() | [trans_imp_sp_trans_a] |
![]() ![]() ![]() ![]() ![]() Thm* (Trans a,b:T. R(a,b)) ![]() ![]() | [trans_imp_sp_trans] |
![]() ![]() ![]() ![]() ![]() Thm* Order(T;x,y.R(x,y)) Thm* ![]() ![]() Thm* ( ![]() Thm* ![]() ![]() Thm* ( ![]() ![]() ![]() ![]() | [order_split] |
![]() ![]() ![]() ![]() ![]() Thm* ( ![]() ![]() ![]() Thm* ![]() ![]() Thm* (Linorder(T;x,y.R(x,y)) ![]() ![]() | [linorder_functionality_wrt_iff] |
![]() ![]() ![]() ![]() ![]() Thm* ( ![]() ![]() ![]() Thm* ![]() ![]() Thm* (Order(T;x,y.R(x,y)) ![]() ![]() | [order_functionality_wrt_iff] |
![]() ![]() ![]() ![]() ![]() Thm* ( ![]() Thm* ![]() ![]() Thm* (Connex(T;x,y.R(x,y)) Thm* ( ![]() ![]() Thm* (( ![]() Thm* ((strict_part(x,y.R(x,y);a;b) Thm* (( ![]() Thm* (( ![]() | [connex_iff_trichot] |
![]() ![]() ![]() ![]() ![]() Thm* ( ![]() ![]() ![]() Thm* ![]() ![]() Thm* Connex(T;x,y.R(x,y)) ![]() ![]() | [connex_functionality_wrt_implies] |
![]() ![]() ![]() ![]() ![]() Thm* ( ![]() ![]() ![]() Thm* ![]() ![]() Thm* (Connex(T;x,y.R(x,y)) ![]() ![]() | [connex_functionality_wrt_iff] |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | [strict_part_irrefl] |
![]() ![]() ![]() ![]() ![]() Thm* ( ![]() ![]() ![]() Thm* ![]() ![]() Thm* (AntiSym(T;x,y.R(x,y)) ![]() ![]() | [anti_sym_functionality_wrt_iff] |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | [squash_thru_equiv_rel] |
![]() ![]() ![]() ![]() ![]() Thm* (EquivRel x,y:T. R(x,y)) Thm* ![]() ![]() Thm* ( ![]() ![]() ![]() ![]() ![]() ![]() ![]() | [equiv_rel_self_functionality] |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* T = T' Thm* ![]() ![]() Thm* ( ![]() ![]() ![]() Thm* ![]() ![]() Thm* ((EquivRel x,y:T. E(x,y)) ![]() ![]() | [equiv_rel_functionality_wrt_iff] |
![]() ![]() | [equiv_rel_iff] |
![]() ![]() ![]() ![]() ![]() Thm* (Trans x,y:T. R(x,y)) Thm* ![]() ![]() Thm* ( ![]() Thm* (Symmetrize(x,y.R(x,y);a;b) Thm* ( ![]() ![]() Thm* (Symmetrize(x,y.R(x,y);a';b') ![]() ![]() ![]() ![]() | [trans_rel_func_wrt_sym_self] |
![]() ![]() ![]() ![]() ![]() Thm* Preorder(T;x,y.R(x,y)) ![]() ![]() | [symmetrized_preorder] |
![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* (EquivRel x,y:T. R(x,y)) ![]() ![]() | [equiv_rel_subtyping] |
![]() ![]() ![]() ![]() ![]() Thm* (Trans x,y:T. R(x,y)) Thm* ![]() ![]() Thm* ( ![]() ![]() ![]() ![]() ![]() ![]() ![]() | [trans_rel_self_functionality] |
![]() ![]() ![]() ![]() ![]() Thm* ( ![]() ![]() ![]() Thm* ![]() ![]() Thm* ((Trans y,x:T. R(x,y)) ![]() ![]() | [trans_functionality_wrt_iff] |
![]() ![]() ![]() ![]() ![]() Thm* ( ![]() ![]() ![]() Thm* ![]() ![]() Thm* ((Sym x,y:T. R(x,y)) ![]() ![]() | [sym_functionality_wrt_iff] |
![]() ![]() ![]() ![]() ![]() Thm* ( ![]() ![]() ![]() ![]() ![]() ![]() ![]() | [refl_functionality_wrt_iff] |
In prior sections: core well fnd int 1 bool 1
Try larger context:
StandardLIB
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html