Definition:Relation Segment

It has been suggested that this page or section be merged into Definition:Preimage/Relation/Element. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Mergeto}} from the code.

Definition

Let $X$ be a set.

Let $\RR$ be a relation on $X$.

Let $x \in X$.

Then the $\RR$-segment of $x$, denoted by $x^\RR$, is defined by:

$x^\RR := \set {y \in X: \tuple {y, x} \in \RR}$

Sources

• Mizar article WAYBEL_4:def 10