Definition:Approximating Relation

Definition

Let $L = \struct {S, \preceq}$ be an ordered set.

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

Then $\RR$ is an approximating relation on $S$ if and only if

$\forall x \in S: x = \map \sup {x^\RR}$

where $x^\RR$ denotes the $\RR$-segment of $x$.

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 17