(set-of [x T] (exists [y U] (R x y)))

Definition: The domain of relation R.

(lambda [x T] (lambda [y U] p/absurd))

Definition: The empty relation.

(forall [x T] (forall [y U] (not ((emptyrel T U) x y))))

Theorem:

(lambda [x T] (lambda [y U] p/truth))

Definition: The full (total) relation between T and U.

(forall [x T] (forall [y U] ((fullrel T U) x y)))

Theorem:

(forall [x T] (q/unique (lambda [y U] (R x y))))

Definition:

(lambda [x T] (lambda [y U] (equal (f x) y)))

Definition: The relation corresponding to function f.

(functional (funrel f))

Theorem:

(reflexive (identity T))

Theorem:

(symmetric (identity T))

Theorem:

(transitive (identity T))

Theorem:

(lambda [x y T] (equal x y))

Definition: The indentity relation on T.

(lambda [x T] (lambda [y U] (and (elem x s1) (elem y s2))))

Definition: The cartersian product of sets s1 and s2, i.e. s1⨯s2.

(and (subrel R1 R2) (not (releq R1 R2)))

Definition: The anti-reflexive variant of subrel.

(not (psubrel R R))

Theorem:

(not (and (psubrel R1 R2) (psubrel R2 R1)))

Theorem:

(==> (psubrel (emptyrel T U) R) (not (releq R (emptyrel T U))))

Theorem:

(==> (not (releq R (emptyrel T U))) (psubrel (emptyrel T U) R))

Theorem:

(<=> (psubrel (emptyrel T U) R) (not (releq R (emptyrel T U))))

Theorem:

(==> (psubrel R1 R2) (psubrel R2 R3) (psubrel R1 R3))

Theorem:

(set-of [y U] (exists [x T] (R x y)))

Definition: The range of relation R.

(lambda [x T] (lambda [z V] (exists [y U] (and (R1 x y) (R2 y z)))))

Definition: Sequential relational composition.

(releq (rcomp R1 (rcomp R2 R3)) (rcomp (rcomp R1 R2) R3))

Theorem: Relational composition is associative.

(subrel (rcomp R1 (rcomp R2 R3)) (rcomp (rcomp R1 R2) R3))

Theorem:

(subrel (rcomp (rcomp R1 R2) R3) (rcomp R1 (rcomp R2 R3)))

Theorem:

(lambda [x y T] (or (R x y) (equal x y)))

Definition: The reflexive closure of relation R.

(forall
 [S (rel T T)]
 (==> (subrel R S) (reflexive S) (subrel (refl-closure R) S)))

Theorem:

(subrel R (refl-closure R))

Theorem:

(forall [x T] (R x x))

Definition: A reflexive relation.

(reflexive (refl-closure R))

Theorem:

(==> T U :type)

Definition: The type of relations.

(forall [P (==> (rel T U) :type)] (<=> (P R1) (P R2)))

Definition: A Leibniz-stype equality for relations.

It says that two relations R1 and R2 are equal iff for any predicate P then (P R1) if and only if (P R2).

Note that the identification with seteq is non-trivial, and requires an axiom.

(==> (rel-equal R1 R2) (releq R1 R2))

Theorem:

(==> (rel-equal R1 R2) (subrel R1 R2))

Theorem:

(==> (rel-equal R1 R2) (P R1) (P R2))

Theorem:

(rel-equal R R)

Theorem:

(<=> (rel-equal R1 R2) (releq R1 R2))

Theorem: Coincidence of Leibniz-style and subset-based equality for relations.

(==> (rel-equal R1 R2) (rel-equal R2 R1))

Theorem:

(==> (rel-equal R1 R2) (rel-equal R2 R3) (rel-equal R1 R3))

Theorem:

(and (subrel R1 R2) (subrel R2 R1))

Definition: Subset-based equality on relations.

(==> (releq R1 R2) (rel-equal R1 R2))

Axiom: As for the set case (cf. sets/seteq-implies-set-equal), going from the subset-based equality to the (thus more general) leibniz-style one requires an axiom.

(releq R R)

Theorem:

(==> (releq R1 R2) (releq R2 R1))

Theorem:

(==> (releq R1 R2) (releq R2 R3) (releq R1 R3))

Theorem:

(lambda [x T] (q/the (fproof x)))

Definition: The function corresponding to a total, functional relation.

(forall
 [x T]
 (forall [y U] (==> (R x y) (equal ((relfun R fproof) x) y))))

Theorem: The image of a functional relation

(forall [x T] (R x ((relfun R fproof) x)))

Theorem: The property of the relational/functional image.

(equal f (relfun (funrel f) (funrel-functional f)))

Theorem: This is the intentional variant of relfunrel-ext-equal.

(forall
 [x T]
 (equal (f x) ((relfun (funrel f) (funrel-functional f)) x)))

Theorem: This is the extensional equality of a function f and its relational characterization.

(forall [x T] (forall [y U] (==> (R1 x y) (R2 x y))))

Definition: The subset ordering for relations, i.e. R1⊆R2

(subrel (emptyrel T U) R)

Theorem: The empty relation is a subset of every other relations.

(subrel R (fullrel T U))

Theorem: The full relation is a superset of every other relations.

(==>
 (forall [x T] (forall [y U] (==> (R2 x y) (P x y))))
 (subrel R1 R2)
 (forall [x T] (forall [y U] (==> (R1 x y) (P x y)))))

Theorem: Preservation of properties on relational subsets.

(subrel R R)

Theorem:

(==> (subrel R1 R2) (subrel R2 R3) (subrel R1 R3))

Theorem:

(lambda [x y T] (or (R x y) (R y x)))

Definition: The symmetric closure of relation R.

(forall
 [S (rel T T)]
 (==> (subrel R S) (symmetric S) (subrel (symm-closure R) S)))

Theorem:

(subrel R (symm-closure R))

Theorem:

(forall [x y T] (==> (R x y) (R y x)))

Definition: A symmetric relation.

(symmetric (symm-closure R))

Theorem:

(forall [x y z T] (==> (R x y) (R y z) (R x z)))

Definition: A transitive relation.