Over and Under

Relation division

Right division (Over)

Overβ€…β€ŠAβ€…β€ŠBβ€…β€ŠCβ€…β€ŠXβ€…β€ŠY:={β€…β€Ša∈A,c∈C:βˆ€(b∈B:(b,a)∈Y:(b,c)∈X):(a,c)β€…β€Š}\textbf{Over} \; A \; B \; C \; X \; Y := \{\; a \in A, c \in C : \forall( b\in B : (b,a) \in Y : (b,c) \in X) : (a,c) \;\}

Relationβ€…β€ŠBβ€…β€ŠAβ€…β€ŠX\textbf{Relation} \; B \; A \; X

Relationβ€…β€ŠBβ€…β€ŠCβ€…β€ŠY\textbf{Relation} \; B \; C \; Y


Notation.

  1. Overβ€…β€ŠAβ€…β€ŠBβ€…β€ŠCβ€…β€ŠXβ€…β€ŠY\textbf{Over} \; A \; B \; C \; X \; Y can be written Overβ€…β€ŠXβ€…β€ŠY\textbf{Over} \; X \; Y when AA, BB and CC are clear from the context.

  2. Overβ€…β€ŠXβ€…β€ŠY\textbf{Over} \; X \; Y is written in symbols as X/YX / Y.


fun Over(A,B,C: set univ, X: B->C, Y: B->A) : A->C {
  { a: A, c: C | all b: B | b->a in Y implies b->c in X }
}

Left division (Under)

Underβ€…β€ŠAβ€…β€ŠBβ€…β€ŠCβ€…β€ŠXβ€…β€ŠY:={β€…β€Šc∈C,a∈A:βˆ€(b∈B:(a,b)∈X:(c,b)∈Y):(c,a)β€…β€Š}\textbf{Under} \; A \; B \; C \; X \; Y := \{\; c \in C, a \in A : \forall( b\in B : (a,b) \in X : (c,b) \in Y ) : (c,a)\;\}

Relationβ€…β€ŠAβ€…β€ŠBβ€…β€ŠX\textbf{Relation} \; A \; B \; X

Relationβ€…β€ŠCβ€…β€ŠBβ€…β€ŠY\textbf{Relation} \; C \; B \; Y


Notation.

  1. Underβ€…β€ŠAβ€…β€ŠBβ€…β€ŠCβ€…β€ŠXβ€…β€ŠY\textbf{Under} \; A \; B \; C \; X \; Ycan be written Underβ€…β€ŠXβ€…β€ŠY\textbf{Under} \; X \; Ywhen AA, BB and CC are clear from the context.

  2. Underβ€…β€ŠXβ€…β€ŠY\textbf{Under} \; X \; Y is written in symbols as X\YX \backslash Y.


fun Under(A,B,C: set univ, X: A->B, Y: C->B) : C->A {
  { c: C, a: A | all b: B | a->b in X implies c->b in Y }
}

Last updated