sets_1 Theory

Summary of Definitions

Typed Definitions

poset_sig *1

set_car *1

set_eq *1

set_le *1

dset *1

mk_dset *3

set_leq *1

set_blt *1

set_lt *1

qoset *1

poset *1

loset *1

mk_oset *6

eq_pair *1

set_prod *4

dset_set *4

int_loset *7

atom_dset *3

Main Theorems

assert_of_dset_eq *4

decidable__dset_eq *2

dset_eq_refl *3

decidable__set_leq *1

assert_of_set_leq *1

set_lt_is_sp_of_leq *3

set_lt_is_sp_of_leq_a *3

decidable__set_lt *1

assert_of_set_lt *1

qoset_refl *1

set_leq_weakening_eq *3

qoset_trans *1

set_leq_transitivity *1

set_leq_trans *2

qoset_lt_trans *2

qoset_lt_irrefl *3

set_lt_irreflexivity *2

set_leq_weakening_lt *3

set_lt_transitivity_1 *3

set_lt_transitivity_2 *3

set_blt_functionality_wrt_set_lt_r *3

poset_anti_sym *1

set_leq_antisymmetry *1

set_leq_iff_lt_or_eq *7

loset_connex *1

loset_trichot *13

set_leq_complement *5

set_lt_complement *6

assert_of_eq_pair *8