Theory "set_relation"

Parents pred_set

Signature

Constant	Type
RREFL_EXP	:α reln -> (α -> bool) -> α reln
RRUNIV	:(α -> bool) -> α reln
acyclic	:α reln -> bool
all_choices	:((α -> bool) -> bool) -> (α -> bool) -> bool
antisym	:α reln -> bool
chain	:(α -> bool) -> α reln -> bool
domain	:(α # β -> bool) -> α -> bool
fchains	:α reln -> (α -> bool) -> bool
finite_prefixes	:(α # β -> bool) -> (β -> bool) -> bool
get_min	:α reln -> (α -> bool) # α reln -> α option
irreflexive	:α reln -> (α -> bool) -> bool
linear_order	:α reln -> (α -> bool) -> bool
maximal_elements	:(α -> bool) -> α reln -> α -> bool
minimal_elements	:(α -> bool) -> α reln -> α -> bool
nth_min	:α reln -> (α -> bool) # α reln -> num -> α option
nth_min_tupled	:α reln # ((α -> bool) # α reln) # num -> α option
num_order	:(α -> num) -> (α -> bool) -> α reln
partial_order	:α reln -> (α -> bool) -> bool
per	:(α -> bool) -> ((α -> bool) -> bool) -> bool
per_restrict	:((α -> bool) -> bool) -> (α -> bool) reln
range	:(β # α -> bool) -> α -> bool
rcomp	:(α # γ -> bool) -> (γ # β -> bool) -> α # β -> bool
reflexive	:α reln -> (α -> bool) -> bool
rel_to_reln	:(α -> β -> bool) -> α # β -> bool
reln_to_rel	:(α # β -> bool) -> α -> β -> bool
rrestrict	:α reln -> (α -> bool) -> α reln
strict	:α reln -> α reln
strict_linear_order	:α reln -> (α -> bool) -> bool
tc	:α reln -> α reln
transitive	:α reln -> bool
univ_reln	:(α -> bool) -> α reln
upper_bounds	:(β -> bool) -> (β # α -> bool) -> α -> bool

Definitions

domain_def

|- ∀r. domain r = {x | ∃y. (x,y) ∈ r}

range_def

|- ∀r. range r = {y | ∃x. (x,y) ∈ r}

rrestrict_def

|- ∀r s. rrestrict r s = {(x,y) | (x,y) ∈ r ∧ x ∈ s ∧ y ∈ s}

rcomp_def

|- ∀r1 r2. r1 OO r2 = {(x,y) | ∃z. (x,z) ∈ r1 ∧ (z,y) ∈ r2}

strict_def

|- ∀r. strict r = {(x,y) | (x,y) ∈ r ∧ x ≠ y}

univ_reln_def

|- ∀xs. univ_reln xs = {(x1,x2) | x1 ∈ xs ∧ x2 ∈ xs}

finite_prefixes_def

|- ∀r s. finite_prefixes r s ⇔ ∀e. e ∈ s ⇒ FINITE {e' | (e',e) ∈ r}

tc_def

|- tc =
   (λr a0.
      ∀tc'.
        (∀a0.
           (∃x y. (a0 = (x,y)) ∧ r (x,y)) ∨
           (∃x y. (a0 = (x,y)) ∧ ∃z. tc' (x,z) ∧ tc' (z,y)) ⇒
           tc' a0) ⇒
        tc' a0)

acyclic_def

|- ∀r. acyclic r ⇔ ∀x. (x,x) ∉ tc r

maximal_elements_def

|- ∀xs r.
     maximal_elements xs r =
     {x | x ∈ xs ∧ ∀x'. x' ∈ xs ∧ (x,x') ∈ r ⇒ (x = x')}

minimal_elements_def

|- ∀xs r.
     minimal_elements xs r =
     {x | x ∈ xs ∧ ∀x'. x' ∈ xs ∧ (x',x) ∈ r ⇒ (x = x')}

reflexive_def

|- ∀r s. reflexive r s ⇔ ∀x. x ∈ s ⇒ (x,x) ∈ r

irreflexive_def

|- ∀r s. irreflexive r s ⇔ ∀x. x ∈ s ⇒ (x,x) ∉ r

transitive_def

|- ∀r. transitive r ⇔ ∀x y z. (x,y) ∈ r ∧ (y,z) ∈ r ⇒ (x,z) ∈ r

antisym_def

|- ∀r. antisym r ⇔ ∀x y. (x,y) ∈ r ∧ (y,x) ∈ r ⇒ (x = y)

partial_order_def

|- ∀r s.
     partial_order r s ⇔
     domain r ⊆ s ∧ range r ⊆ s ∧ transitive r ∧ reflexive r s ∧ antisym r

linear_order_def

|- ∀r s.
     linear_order r s ⇔
     domain r ⊆ s ∧ range r ⊆ s ∧ transitive r ∧ antisym r ∧
     ∀x y. x ∈ s ∧ y ∈ s ⇒ (x,y) ∈ r ∨ (y,x) ∈ r

strict_linear_order_def

|- ∀r s.
     strict_linear_order r s ⇔
     domain r ⊆ s ∧ range r ⊆ s ∧ transitive r ∧ (∀x. (x,x) ∉ r) ∧
     ∀x y. x ∈ s ∧ y ∈ s ∧ x ≠ y ⇒ (x,y) ∈ r ∨ (y,x) ∈ r

chain_def

|- ∀s r. chain s r ⇔ ∀x y. x ∈ s ∧ y ∈ s ⇒ (x,y) ∈ r ∨ (y,x) ∈ r

upper_bounds_def

|- ∀s r. upper_bounds s r = {x | x ∈ range r ∧ ∀y. y ∈ s ⇒ (y,x) ∈ r}

fchains_def

|- ∀r.
     fchains r =
     {k |
      chain k r ∧ k ≠ ∅ ∧
      ∀C.
        chain C r ∧ C ⊆ k ∧ (upper_bounds C r DIFF C) ∩ k ≠ ∅ ⇒
        CHOICE (upper_bounds C r DIFF C) ∈
        minimal_elements ((upper_bounds C r DIFF C) ∩ k) r}

per_def

|- ∀xs xss.
     per xs xss ⇔
     BIGUNION xss ⊆ xs ∧ ∅ ∉ xss ∧
     ∀xs1 xs2. xs1 ∈ xss ∧ xs2 ∈ xss ∧ xs1 ≠ xs2 ⇒ DISJOINT xs1 xs2

per_restrict_def

|- ∀xss xs. per_restrict xss xs = {xs' ∩ xs | xs' ∈ xss} DELETE ∅

all_choices_def

|- ∀xss.
     all_choices xss =
     {IMAGE choice xss | choice | ∀xs. xs ∈ xss ⇒ choice xs ∈ xs}

num_order_def

|- ∀f s. num_order f s = {(x,y) | x ∈ s ∧ y ∈ s ∧ f x ≤ f y}

get_min_def

|- ∀r' s r.
     get_min r' (s,r) =
     (let mins = minimal_elements (minimal_elements s r) r'
      in
        if SING mins then SOME (CHOICE mins) else NONE)

nth_min_tupled_primitive_def

|- nth_min_tupled =
   WFREC
     (@R.
        WF R ∧
        ∀n r s r' min.
          (min = get_min r' (s,r)) ∧ min ≠ NONE ⇒
          R (r',(s DELETE THE min,r),n) (r',(s,r),SUC n))
     (λnth_min_tupled a.
        case a of
          (r',(s,r),0) => I (get_min r' (s,r))
        | (r',(s,r),SUC n) =>
            I
              (let min = get_min r' (s,r)
               in
                 if min = NONE then NONE
                 else nth_min_tupled (r',(s DELETE THE min,r),n)))

nth_min_curried_def

|- ∀x x1 x2. nth_min x x1 x2 = nth_min_tupled (x,x1,x2)

reln_to_rel_def

|- ∀r. reln_to_rel r = (λx y. (x,y) ∈ r)

rel_to_reln_def

|- ∀R. rel_to_reln R = {(x,y) | R x y}

RRUNIV_def

|- ∀s. RRUNIV s = (λx y. x ∈ s ∧ y ∈ s)

RREFL_EXP_def

|- ∀R s. RREFL_EXP R s = R RUNION (λx y. (x = y) ∧ x ∉ s)

Theorems

reflexive_reln_to_rel_conv_UNIV

|- reflexive r 𝕌(:α) ⇔ reflexive (reln_to_rel r)

rcomp_to_rel_conv

|- r1 OO r2 = rel_to_reln (reln_to_rel r2 O reln_to_rel r1)

acyclic_bigunion

|- ∀rs.
     (∀r r'.
        r ∈ rs ∧ r' ∈ rs ∧ r ≠ r' ⇒
        DISJOINT (domain r ∪ range r) (domain r' ∪ range r')) ∧
     (∀r. r ∈ rs ⇒ acyclic r) ⇒
     acyclic (BIGUNION rs)

acyclic_irreflexive

|- ∀r x. acyclic r ⇒ (x,x) ∉ r

acyclic_rrestrict

|- ∀r s. acyclic r ⇒ acyclic (rrestrict r s)

tc_ind

|- ∀r tc'.
     (∀x y. (x,y) ∈ r ⇒ tc' x y) ∧ (∀x y. (∃z. tc' x z ∧ tc' z y) ⇒ tc' x y) ⇒
     ∀x y. (x,y) ∈ tc r ⇒ tc' x y

rextension

|- ∀s t. (s = t) ⇔ ∀x y. (x,y) ∈ s ⇔ (x,y) ∈ t

in_domain

|- ∀x r. x ∈ domain r ⇔ ∃y. (x,y) ∈ r

in_range

|- ∀y r. y ∈ range r ⇔ ∃x. (x,y) ∈ r

in_rrestrict

|- ∀x y r s. (x,y) ∈ rrestrict r s ⇔ (x,y) ∈ r ∧ x ∈ s ∧ y ∈ s

rrestrict_union

|- ∀r1 r2 s. rrestrict (r1 ∪ r2) s = rrestrict r1 s ∪ rrestrict r2 s

rrestrict_rrestrict

|- ∀r x y. rrestrict (rrestrict r x) y = rrestrict r (x ∩ y)

strict_rrestrict

|- ∀r s. strict (rrestrict r s) = rrestrict (strict r) s

finite_prefixes_subset

|- ∀r s s'.
     finite_prefixes r s ∧ s' ⊆ s ⇒
     finite_prefixes r s' ∧ finite_prefixes (rrestrict r s') s'

finite_prefixes_union

|- ∀r1 r2 s1 s2.
     finite_prefixes r1 s1 ∧ finite_prefixes r2 s2 ⇒
     finite_prefixes (r1 ∪ r2) (s1 ∩ s2)

finite_prefixes_comp

|- ∀r1 r2 s1 s2.
     finite_prefixes r1 s1 ∧ finite_prefixes r2 s2 ∧
     {x | ∃y. y ∈ s2 ∧ (x,y) ∈ r2} ⊆ s1 ⇒
     finite_prefixes (r1 OO r2) s2

finite_prefixes_inj_image

|- ∀f r s.
     (∀x y. (f x = f y) ⇒ (x = y)) ∧ finite_prefixes r s ⇒
     finite_prefixes {(f x,f y) | (x,y) ∈ r} (IMAGE f s)

finite_prefixes_range

|- ∀r s t.
     finite_prefixes r s ∧ DISJOINT t (range r) ⇒ finite_prefixes r (s ∪ t)

tc_rules

|- ∀r.
     (∀x y. (x,y) ∈ r ⇒ (x,y) ∈ tc r) ∧
     ∀x y. (∃z. (x,z) ∈ tc r ∧ (z,y) ∈ tc r) ⇒ (x,y) ∈ tc r

tc_cases

|- ∀r x y. (x,y) ∈ tc r ⇔ (x,y) ∈ r ∨ ∃z. (x,z) ∈ tc r ∧ (z,y) ∈ tc r

tc_strongind

|- ∀r tc'.
     (∀x y. (x,y) ∈ r ⇒ tc' x y) ∧
     (∀x y. (∃z. (x,z) ∈ tc r ∧ tc' x z ∧ (z,y) ∈ tc r ∧ tc' z y) ⇒ tc' x y) ⇒
     ∀x y. (x,y) ∈ tc r ⇒ tc' x y

tc_cases_right

|- ∀r x y. (x,y) ∈ tc r ⇔ (x,y) ∈ r ∨ ∃z. (x,z) ∈ tc r ∧ (z,y) ∈ r

tc_cases_left

|- ∀r x y. (x,y) ∈ tc r ⇔ (x,y) ∈ r ∨ ∃z. (x,z) ∈ r ∧ (z,y) ∈ tc r

tc_ind_left

|- ∀r tc'.
     (∀x y. (x,y) ∈ r ⇒ tc' x y) ∧
     (∀x y. (∃z. (x,z) ∈ r ∧ tc' z y) ⇒ tc' x y) ⇒
     ∀x y. (x,y) ∈ tc r ⇒ tc' x y

tc_strongind_left

|- ∀r tc'.
     (∀x y. (x,y) ∈ r ⇒ tc' x y) ∧
     (∀x y. (∃z. (x,z) ∈ r ∧ (z,y) ∈ tc r ∧ tc' z y) ⇒ tc' x y) ⇒
     ∀x y. (x,y) ∈ tc r ⇒ tc' x y

tc_ind_right

|- ∀r tc'.
     (∀x y. (x,y) ∈ r ⇒ tc' x y) ∧
     (∀x y. (∃z. tc' x z ∧ (z,y) ∈ r) ⇒ tc' x y) ⇒
     ∀x y. (x,y) ∈ tc r ⇒ tc' x y

rtc_ind_right

|- ∀r tc'.
     (∀x. x ∈ domain r ∨ x ∈ range r ⇒ tc' x x) ∧
     (∀x y. (∃z. tc' x z ∧ (z,y) ∈ r) ⇒ tc' x y) ⇒
     ∀x y. (x,y) ∈ tc r ⇒ tc' x y

tc_strongind_right

|- ∀r tc'.
     (∀x y. (x,y) ∈ r ⇒ tc' x y) ∧
     (∀x y. (∃z. (x,z) ∈ tc r ∧ tc' x z ∧ (z,y) ∈ r) ⇒ tc' x y) ⇒
     ∀x y. (x,y) ∈ tc r ⇒ tc' x y

tc_union

|- ∀x y. (x,y) ∈ tc r1 ⇒ ∀r2. (x,y) ∈ tc (r1 ∪ r2)

tc_implication

|- ∀r1 r2.
     (∀x y. (x,y) ∈ r1 ⇒ (x,y) ∈ r2) ⇒ ∀x y. (x,y) ∈ tc r1 ⇒ (x,y) ∈ tc r2

tc_empty

|- ∀x y. (x,y) ∉ tc ∅

tc_domain_range

|- ∀x y. (x,y) ∈ tc r ⇒ x ∈ domain r ∧ y ∈ range r

rrestrict_tc

|- ∀e e'. (e,e') ∈ tc (rrestrict r x) ⇒ (e,e') ∈ tc r

acyclic_subset

|- ∀r1 r2. acyclic r1 ∧ r2 ⊆ r1 ⇒ acyclic r2

acyclic_union

|- ∀r r'.
     DISJOINT (domain r ∪ range r) (domain r' ∪ range r') ∧ acyclic r ∧
     acyclic r' ⇒
     acyclic (r ∪ r')

maximal_union

|- ∀e s r1 r2.
     e ∈ maximal_elements s (r1 ∪ r2) ⇒
     e ∈ maximal_elements s r1 ∧ e ∈ maximal_elements s r2

minimal_union

|- ∀e s r1 r2.
     e ∈ minimal_elements s (r1 ∪ r2) ⇒
     e ∈ minimal_elements s r1 ∧ e ∈ minimal_elements s r2

finite_acyclic_has_maximal

|- ∀s. FINITE s ⇒ s ≠ ∅ ⇒ ∀r. acyclic r ⇒ ∃x. x ∈ maximal_elements s r

finite_acyclic_has_minimal

|- ∀s. FINITE s ⇒ s ≠ ∅ ⇒ ∀r. acyclic r ⇒ ∃x. x ∈ minimal_elements s r

maximal_TC

|- ∀s r.
     domain r ⊆ s ∧ range r ⊆ s ⇒
     (maximal_elements s (tc r) = maximal_elements s r)

minimal_TC

|- ∀s r.
     domain r ⊆ s ∧ range r ⊆ s ⇒
     (minimal_elements s (tc r) = minimal_elements s r)

finite_acyclic_has_maximal_path

|- ∀s r x.
     FINITE s ∧ acyclic r ∧ x ∈ s ∧ x ∉ maximal_elements s r ⇒
     ∃y. y ∈ maximal_elements s r ∧ (x,y) ∈ tc r

finite_acyclic_has_minimal_path

|- ∀s r x.
     FINITE s ∧ acyclic r ∧ x ∈ s ∧ x ∉ minimal_elements s r ⇒
     ∃y. y ∈ minimal_elements s r ∧ (y,x) ∈ tc r

transitive_tc

|- ∀r. transitive r ⇒ (tc r = r)

tc_transitive

|- ∀r. transitive (tc r)

partial_order_dom_rng

|- ∀r s x y. (x,y) ∈ r ∧ partial_order r s ⇒ x ∈ s ∧ y ∈ s

partial_order_subset

|- ∀r s s'. partial_order r s ∧ s' ⊆ s ⇒ partial_order (rrestrict r s') s'

strict_partial_order

|- ∀r s.
     partial_order r s ⇒
     domain (strict r) ⊆ s ∧ range (strict r) ⊆ s ∧ transitive (strict r) ∧
     antisym (strict r)

strict_partial_order_acyclic

|- ∀r s. partial_order r s ⇒ acyclic (strict r)

finite_prefix_po_has_minimal_path

|- ∀r s x s'.
     partial_order r s ∧ finite_prefixes r s ∧ x ∉ minimal_elements s' r ∧
     x ∈ s' ∧ s' ⊆ s ⇒
     ∃x'. x' ∈ minimal_elements s' r ∧ (x',x) ∈ r

linear_order_subset

|- ∀r s s'. linear_order r s ∧ s' ⊆ s ⇒ linear_order (rrestrict r s') s'

partial_order_linear_order

|- ∀r s. linear_order r s ⇒ partial_order r s

strict_linear_order_dom_rng

|- ∀r s x y. (x,y) ∈ r ∧ strict_linear_order r s ⇒ x ∈ s ∧ y ∈ s

linear_order_dom_rng

|- ∀r s x y. (x,y) ∈ r ∧ linear_order r s ⇒ x ∈ s ∧ y ∈ s

empty_strict_linear_order

|- ∀r. strict_linear_order r ∅ ⇔ (r = ∅)

empty_linear_order

|- ∀r. linear_order r ∅ ⇔ (r = ∅)

linear_order_restrict

|- ∀s r s'. linear_order r s ⇒ linear_order (rrestrict r s') (s ∩ s')

strict_linear_order_restrict

|- ∀s r s'.
     strict_linear_order r s ⇒ strict_linear_order (rrestrict r s') (s ∩ s')

extend_linear_order

|- ∀r s x.
     x ∉ s ∧ linear_order r s ⇒
     linear_order (r ∪ {(y,x) | y | y ∈ s ∪ {x}}) (s ∪ {x})

strict_linear_order_acyclic

|- ∀r s. strict_linear_order r s ⇒ acyclic r

strict_linear_order_union_acyclic

|- ∀r1 r2 s.
     strict_linear_order r1 s ∧ domain r2 ∪ range r2 ⊆ s ⇒
     (acyclic (r1 ∪ r2) ⇔ r2 ⊆ r1)

strict_linear_order

|- ∀r s. linear_order r s ⇒ strict_linear_order (strict r) s

linear_order

|- ∀r s. strict_linear_order r s ⇒ linear_order (r ∪ {(x,x) | x ∈ s}) s

finite_strict_linear_order_has_maximal

|- ∀s r.
     FINITE s ∧ strict_linear_order r s ∧ s ≠ ∅ ⇒ ∃x. x ∈ maximal_elements s r

finite_strict_linear_order_has_minimal

|- ∀s r.
     FINITE s ∧ strict_linear_order r s ∧ s ≠ ∅ ⇒ ∃x. x ∈ minimal_elements s r

finite_linear_order_has_maximal

|- ∀s r. FINITE s ∧ linear_order r s ∧ s ≠ ∅ ⇒ ∃x. x ∈ maximal_elements s r

finite_linear_order_has_minimal

|- ∀s r. FINITE s ∧ linear_order r s ∧ s ≠ ∅ ⇒ ∃x. x ∈ minimal_elements s r

maximal_linear_order

|- ∀s r x y. y ∈ s ∧ linear_order r s ∧ x ∈ maximal_elements s r ⇒ (y,x) ∈ r

minimal_linear_order

|- ∀s r x y. y ∈ s ∧ linear_order r s ∧ x ∈ minimal_elements s r ⇒ (x,y) ∈ r

minimal_linear_order_unique

|- ∀r s s' x y.
     linear_order r s ∧ x ∈ minimal_elements s' r ∧
     y ∈ minimal_elements s' r ∧ s' ⊆ s ⇒
     (x = y)

finite_prefix_linear_order_has_unique_minimal

|- ∀r s s'.
     linear_order r s ∧ finite_prefixes r s ∧ x ∈ s' ∧ s' ⊆ s ⇒
     SING (minimal_elements s' r)

nat_order_iso_thm

|- ∀f s.
     (∀n m. (f m = f n) ∧ f m ≠ NONE ⇒ (m = n)) ∧
     (∀x. x ∈ s ⇒ ∃m. f m = SOME x) ∧ (∀m x. (f m = SOME x) ⇒ x ∈ s) ⇒
     linear_order {(x,y) | ∃m n. m ≤ n ∧ (f m = SOME x) ∧ (f n = SOME y)} s ∧
     finite_prefixes {(x,y) | ∃m n. m ≤ n ∧ (f m = SOME x) ∧ (f n = SOME y)} s

upper_bounds_lem

|- ∀r s x1 x2.
     transitive r ∧ x1 ∈ upper_bounds s r ∧ (x1,x2) ∈ r ⇒
     x2 ∈ upper_bounds s r

zorns_lemma

|- ∀r s.
     s ≠ ∅ ∧ partial_order r s ∧ (∀t. chain t r ⇒ upper_bounds t r ≠ ∅) ⇒
     ∃x. x ∈ maximal_elements s r

per_delete

|- ∀xs xss e.
     per xs xss ⇒
     per (xs DELETE e) {es | es ∈ IMAGE (λes. es DELETE e) xss ∧ es ≠ ∅}

per_restrict_per

|- ∀r s s'. per s r ⇒ per s' (per_restrict r s')

countable_per

|- ∀xs xss. countable xs ∧ per xs xss ⇒ countable xss

all_choices_thm

|- ∀x s y. x ∈ all_choices s ∧ y ∈ x ⇒ ∃z. z ∈ s ∧ y ∈ z

linear_order_num_order

|- ∀f s t. INJ f s t ⇒ linear_order (num_order f s) s

num_order_finite_prefix

|- ∀f s t. INJ f s t ⇒ finite_prefixes (num_order f s) s

nth_min_ind

|- ∀P.
     (∀r' s r. P r' (s,r) 0) ∧
     (∀r' s r n.
        (∀min.
           (min = get_min r' (s,r)) ∧ min ≠ NONE ⇒
           P r' (s DELETE THE min,r) n) ⇒
        P r' (s,r) (SUC n)) ⇒
     ∀v v1 v2 v3. P v (v1,v2) v3

nth_min_def

|- (∀s r' r. nth_min r' (s,r) 0 = get_min r' (s,r)) ∧
   ∀s r' r n.
     nth_min r' (s,r) (SUC n) =
     (let min = get_min r' (s,r)
      in
        if min = NONE then NONE else nth_min r' (s DELETE THE min,r) n)

nth_min_def_compute

|- (∀s r' r. nth_min r' (s,r) 0 = get_min r' (s,r)) ∧
   (∀s r' r n.
      nth_min r' (s,r) (NUMERAL (BIT1 n)) =
      (let min = get_min r' (s,r)
       in
         if min = NONE then NONE
         else nth_min r' (s DELETE THE min,r) (NUMERAL (BIT1 n) − 1))) ∧
   ∀s r' r n.
     nth_min r' (s,r) (NUMERAL (BIT2 n)) =
     (let min = get_min r' (s,r)
      in
        if min = NONE then NONE
        else nth_min r' (s DELETE THE min,r) (NUMERAL (BIT1 n)))

linear_order_of_countable_po

|- ∀r s.
     countable s ∧ partial_order r s ∧ finite_prefixes r s ⇒
     ∃r'. linear_order r' s ∧ finite_prefixes r' s ∧ r ⊆ r'

RREFL_EXP_RSUBSET

|- R RSUBSET RREFL_EXP R s

RREFL_EXP_UNIV

|- RREFL_EXP R 𝕌(:α) = R

REL_RESTRICT_UNIV

|- REL_RESTRICT R 𝕌(:α) = R

in_rel_to_reln

|- xy ∈ rel_to_reln R ⇔ R (FST xy) (SND xy)

reln_to_rel_app

|- reln_to_rel r x y ⇔ (x,y) ∈ r

rel_to_reln_inv

|- reln_to_rel (rel_to_reln R) = R

reln_to_rel_inv

|- rel_to_reln (reln_to_rel r) = r

reln_to_rel_11

|- (reln_to_rel r1 = reln_to_rel r2) ⇔ (r1 = r2)

rel_to_reln_11

|- (rel_to_reln R1 = rel_to_reln R2) ⇔ (R1 = R2)

rel_to_reln_swap

|- (r = rel_to_reln R) ⇔ (reln_to_rel r = R)

domain_to_rel_conv

|- domain r = RDOM (reln_to_rel r)

range_to_rel_conv

|- range r = RRANGE (reln_to_rel r)

strict_to_rel_conv

|- strict r = rel_to_reln (STRORD (reln_to_rel r))

rrestrict_to_rel_conv

|- univ_reln s = rel_to_reln (RRUNIV s)

tc_to_rel_conv

|- tc r = rel_to_reln (reln_to_rel r)⁺

acyclic_reln_to_rel_conv

|- acyclic r ⇔ irreflexive (reln_to_rel r)⁺

irreflexive_reln_to_rel_conv

|- irreflexive r s ⇔ irreflexive (REL_RESTRICT (reln_to_rel r) s)

irreflexive_reln_to_rel_conv_UNIV

|- irreflexive r 𝕌(:α) ⇔ irreflexive (reln_to_rel r)

reflexive_reln_to_rel_conv

|- transitive r ⇔ transitive (reln_to_rel r)

antisym_reln_to_rel_conv

|- antisym r ⇔ antisymmetric (reln_to_rel r)

partial_order_reln_to_rel_conv

|- partial_order r s ⇔
   reln_to_rel r RSUBSET RRUNIV s ∧ WeakOrder (RREFL_EXP (reln_to_rel r) s)

partial_order_reln_to_rel_conv_UNIV

|- partial_order r 𝕌(:α) ⇔ WeakOrder (reln_to_rel r)

linear_order_reln_to_rel_conv_UNIV

|- linear_order r 𝕌(:α) ⇔ WeakLinearOrder (reln_to_rel r)

strict_linear_order_reln_to_rel_conv_UNIV

|- strict_linear_order r 𝕌(:α) ⇔ StrongLinearOrder (reln_to_rel r)

reln_rel_conv_thms

|- ((xy ∈ rel_to_reln R ⇔ R (FST xy) (SND xy)) ∧
    (reln_to_rel r x y ⇔ (x,y) ∈ r) ∧ (reln_to_rel (rel_to_reln R) = R) ∧
    (rel_to_reln (reln_to_rel r) = r) ∧
    ((reln_to_rel r1 = reln_to_rel r2) ⇔ (r1 = r2)) ∧
    ((rel_to_reln R1 = rel_to_reln R2) ⇔ (R1 = R2))) ∧
   (RREFL_EXP R 𝕌(:α) = R) ∧ (REL_RESTRICT R 𝕌(:α) = R) ∧
   (domain r = RDOM (reln_to_rel r)) ∧ (range r = RRANGE (reln_to_rel r)) ∧
   (strict r = rel_to_reln (STRORD (reln_to_rel r))) ∧
   (rrestrict r s = rel_to_reln (REL_RESTRICT (reln_to_rel r) s)) ∧
   (r1 OO r2 = rel_to_reln (reln_to_rel r2 O reln_to_rel r1)) ∧
   (univ_reln s = rel_to_reln (RRUNIV s)) ∧
   (tc r = rel_to_reln (reln_to_rel r)⁺) ∧
   (acyclic r ⇔ irreflexive (reln_to_rel r)⁺) ∧
   (irreflexive r s ⇔ irreflexive (REL_RESTRICT (reln_to_rel r) s)) ∧
   (reflexive r s ⇔ reflexive (RREFL_EXP (reln_to_rel r) s)) ∧
   (transitive r ⇔ transitive (reln_to_rel r)) ∧
   (antisym r ⇔ antisymmetric (reln_to_rel r)) ∧
   (partial_order r 𝕌(:α) ⇔ WeakOrder (reln_to_rel r)) ∧
   (linear_order r 𝕌(:α) ⇔ WeakLinearOrder (reln_to_rel r)) ∧
   (strict_linear_order r 𝕌(:α) ⇔ StrongLinearOrder (reln_to_rel r))

acyclic_WF

|- FINITE s ∧ acyclic r ∧ domain r ⊆ s ∧ range r ⊆ s ⇒ WF (reln_to_rel r)