Relation concatenation
Set
context | R∈Rel(X,U) |
context | S∈Rel(V,Y) |
definiendum | ⟨x,y⟩∈S∘R |
postulate | ∃m. ⟨x,m⟩∈R∧⟨m,y⟩∈S |
Discussion
Concatenations/compositions are associative.
A mayority of uses of the relation concatenation is when the relation is functional, i.e. one composes functions alla
g:X→Y, f:Y→Z
then
f∘g:X→Z
(f∘g)(x):=f(g(x))
Notation
If f:X→Y and g:Y→Z are functions, we'll often denote f∘g by fg. This convenient notation will also be used in more elaborate cases. For example, if by f(x) we done the values of a function f:X→R and |⋅| is the function which takes a real to its absolute value, then |f| will denote the name of the function with values |f(x)|.