Entry	Value
Package Name	relation-thm
Count	25
Theorems	big_interr : !s x y. big_interr s x y <=> (!r. r IN s ==> r x y) big_unionr : !s x y. big_unionr s x y <=> (?r. r IN s /\ r x y) emptyr : !x y. ~emptyr x y interr : !r s x y. interr r s x y <=> r x y /\ s x y irreflexive : !r x. irreflexive r ==> ~r x x irreflexive_emptyr : irreflexive emptyr reflexive : !r x. reflexive r ==> r x x reflexive_univr : reflexive univr relation_extension_imp : !r s. (!x y. r x y <=> s x y) ==> r = s relation_to_set : !r x y. x,y IN relation_to_set r <=> r x y relation_to_set_inj : !r s. relation_to_set r = relation_to_set s ==> r = s relation_to_set_to_relation : !r. set_to_relation (relation_to_set r) = r set_to_relation_to_set : !s. relation_to_set (set_to_relation s) = s subrelation : !r s. subrelation r s <=> (!x y. r x y ==> s x y) subrelation_antisym : !r s. subrelation r s /\ subrelation s r ==> r = s subrelation_big_interr : !r s. subrelation r (big_interr s) <=> (!t. t IN s ==> subrelation r t) subrelation_refl : !r. subrelation r r subrelation_trans : !r s t. subrelation r s /\ subrelation s t ==> subrelation r t transitive_closure_smallest : !r s. subrelation r s /\ transitive s ==> subrelation (transitive_closure r) s transitive_closure_subrelation : !r. subrelation r (transitive_closure r) transitive_closure_transitive : !r. transitive (transitive_closure r) transitive_emptyr : transitive emptyr transitive_univr : transitive univr unionr : !r s x y. unionr r s x y <=> r x y \/ s x y univr : !x y. univr x y

Back to main package page