Relation division
Relationβ βBβ βAβ βX\textbf{Relation} \; B \; A \; XRelationBAX
Relationβ βBβ βCβ βY\textbf{Relation} \; B \; C \; YRelationBCY
Notation.
Overβ βAβ βBβ βCβ βXβ βY\textbf{Over} \; A \; B \; C \; X \; YOverABCXY can be written Overβ βXβ βY\textbf{Over} \; X \; YOverXY when AAA, BBB and CCC are clear from the context.
Overβ βXβ βY\textbf{Over} \; X \; YOverXY is written in symbols as X/YX / 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 } }
Relationβ βAβ βBβ βX\textbf{Relation} \; A \; B \; XRelationABX
Relationβ βCβ βBβ βY\textbf{Relation} \; C \; B \; YRelationCBY
Underβ βAβ βBβ βCβ βXβ βY\textbf{Under} \; A \; B \; C \; X \; YUnderABCXYcan be written Underβ βXβ βY\textbf{Under} \; X \; YUnderXYwhen AAA, BBB and CCC are clear from the context.
Underβ βXβ βY\textbf{Under} \; X \; YUnderXY is written in symbols as X\YX \backslash YX\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 1 year ago