gen_algebra_1 Theory

A few unary predicates are defined.

Much of the theory concerns common properties of binary relations. Two developments are given, differing in whether relations with or without arguments are considered more fundamental.

Definitions are given for common properties (e.g. commutativity, associativity) of algebraic operators.

Summary of Definitions

Typed Definitions

p_subset *1

p_equiv *1

detach *1

detach_fun *1

refl *1

sym *1

trans *1

equiv_rel *1

preorder *1

symmetrize *1

eqfun_p *1

anti_sym *1

st_anti_sym *1

connex *1

order *1

linorder *1

strict_part *1

irrefl *1

binrel_eqv *1

binrel_le *1

ab_binrel *1

binrel_ap *1

dec_binrel *1

xxrefl *1

xxsym *1

xxtrans *1

xxsymmetrize *1

xxirrefl *1

xxanti_sym *1

xxst_anti_sym *1

xxconnex *1

xxorder *1

xxlinorder *1

refl_cl *1

sym_cl *1

s_part *1

qprop *3

ident *1

assoc *2

comm *1

inverse *2

bilinear *1

bilinear_p *1

action_p *1

dist_1op_2op_lr *1

fun_thru_1op *1

fun_thru_2op *1

cancel *1

monot *1

monotone *1

rels_iso *1

Main Theorems

exists_det_fun *36

exists_det_fun_a *1

dec_alt_char *15

dec_alt_char_a *16

refl_functionality_wrt_iff *3

sym_functionality_wrt_iff *4

trans_functionality_wrt_iff *3

trans_rel_self_functionality *3

equiv_rel_subtyping *5

symmetrized_preorder *6

equiv_rel_iff *4

equiv_rel_functionality_wrt_iff *9

equiv_rel_self_functionality *12

squash_thru_equiv_rel *8

sq_stable__eqfun_p *2

eqfun_p_subtyping *6

anti_sym_functionality_wrt_iff *4

connex_functionality_wrt_iff *3

connex_functionality_wrt_implies *6

connex_iff_trichot *7

order_functionality_wrt_iff *4

linorder_functionality_wrt_iff *2

sq_stable__refl *1

sq_stable__sym *1

sq_stable__trans *1

sq_stable__anti_sym *1

sq_stable__connex *1

strict_part_irrefl *3

order_split *10

trans_imp_sp_trans *4

trans_imp_sp_trans_a *5

trans_imp_sp_trans_b *4

linorder_le_neg *5

linorder_lt_neg *5

binrel_eqv_transitivity *2

binrel_le_antisymmetry *3

binrel_eqv_weakening *3

binrel_eqv_inversion *2

binrel_eqv_functionality_wrt_breqv *5

binrel_le_transitivity *2

binrel_le_weakening *2

ab_binrel_functionality *3

binrel_ap_functionality_wrt_breqv *3

xxrefl_functionality_wrt_breqv *3

xxsym_functionality_wrt_breqv *4

xxtrans_functionality_wrt_breqv *4

xxanti_sym_functionality_wrt_breqv *4

xxconnex_functionality_wrt_breqv *4

xxorder_functionality_wrt_breqv *4

xxorder_eq_order *3

s_part_functionality_wrt_breqv *3

s_part_char *1

xxorder_split *4

xxtrans_imp_sp_trans *5

refl_cl_is_order *14

irrefl_trans_imp_sasym *4

xxconnex_iff_trichot *4

xxconnex_iff_trichot_a *7

rel_le_refl_cl_sp *7

refl_cl_sp_le_rel *4

refl_cl_sp_cancel *3

rel_le_sp_refl_cl *8

sp_refl_cl_le_rel *5

sp_refl_cl_cancel *2

quot_elim *7

all_quot_elim *10

sq_stable__ident *2

sq_stable__assoc *3

sq_stable__comm *2

sq_stable__inverse *2

sq_stable__bilinear *2

bilinear_comm_elim *4

sq_stable__bilinear_p *1

sq_stable__action_p *1

sq_stable__dist_1op_2op_lr *1

sq_stable__fun_thru_1op *1

sq_stable__fun_thru_2op *1

sq_stable__cancel *1

sq_stable__monot *1

monot_functionality *2

assoc_shift *4

comm_shift *4

cancel_shift *5

eqfun_p_shift *5

sym_shift *2

trans_shift *3

connex_shift *2

anti_sym_shift *2

refl_shift *2

monot_shift *3