Not Preceding implies Approximating Relation and not Preceding

From ProofWiki
Jump to navigation Jump to search



Theorem

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a complete lattice.

Let $x, y \in S$ such that

$x \npreceq y$

Let $\RR$ be an approximating relation on $S$.


Then

$\exists u \in S: \tuple {u, x} \in \RR \land u \npreceq y$


Proof

By definition of approximating relation:

$x = \map \sup {x^\RR}$

By definition of supremum:

$y$ is upper bound for $x^\RR \implies x \preceq y$

By definition of upper bound:

$\exists u \in S: u \in x^\RR \land u \npreceq y$

Thus by definition of $\RR$-segment:

$\exists u \in S: \tuple {u, x} \in \RR \land u \npreceq y$

$\blacksquare$


Sources