Definition:Auxiliary Relation
Jump to navigation
Jump to search
This page has been identified as a candidate for refactoring. In particular:
Pages that reference this one will have to be amended for consistency.
Pages that reference this one will have to be amended for consistency.
Until this has been finished, please leave {{refactor}} in the code.
New contributors: Refactoring is a task which is expected to be undertaken by experienced editors only.
Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$.
Definition
Let $L = \struct {S, \vee, \preceq}$ be a bounded below join semilattice.
Let $\RR \subseteq S \times S$ be a relation on $S$.
Then $\RR$ is an auxiliary relation if and only if
| \((1)\) | $:$ | \(\ds \forall x, y \in S:\) | \(\ds \tuple {x, y} \in \RR \implies x \preceq y \) | |||||
| \((2)\) | $:$ | \(\ds \forall x, y, z, u \in S:\) | \(\ds x \preceq y \land \tuple {y, z} \in \RR \land z \preceq u \implies \tuple {x, u} \in \RR \) | |||||
| \((3)\) | $:$ | \(\ds \forall x, y, z \in S:\) | \(\ds \tuple {x, z} \in \RR \land \tuple {y, z} \in \RR \implies \tuple {x \vee y, z} \in \RR \) | |||||
| \((4)\) | $:$ | \(\ds \forall x \in S:\) | \(\ds \tuple {\bot, x} \in \RR \) |
where $\bot$ denotes the bottom and $\land$ denotes conjunction.
Sources
- 1980: G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M.W. Mislove and D.S. Scott: A Compendium of Continuous Lattices
- Mizar article WAYBEL_4:def 7