Entry	Value
Package Name	relation-def
Count	13
Theorems	big_interr_def : !s. big_interr s = set_to_relation (INTERS (IMAGE relation_to_set s)) big_unionr_def : !s. big_unionr s = set_to_relation (UNIONS (IMAGE relation_to_set s)) emptyr_def : emptyr = set_to_relation {} interr_def : !r s. interr r s = set_to_relation (relation_to_set r INTER relation_to_set s) irreflexive_def : !r. irreflexive r <=> (!x. ~r x x) reflexive_def : !r. reflexive r <=> (!x. r x x) relation_to_set_def : !r. relation_to_set r = {x,y | r x y} set_to_relation_def : !s x y. set_to_relation s x y <=> x,y IN s subrelation_def : !r s. subrelation r s <=> relation_to_set r SUBSET relation_to_set s transitive_closure_def : !r. transitive_closure r = big_interr {s | subrelation r s /\ transitive s} transitive_def : !r. transitive r <=> (!x y z. r x y /\ r y z ==> r x z) unionr_def : !r s. unionr r s = set_to_relation (relation_to_set r UNION relation_to_set s) univr_def : univr = set_to_relation UNIV

Back to main package page