Auxiliary Approximating Relation has Quasi Interpolation Property

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $L = \left({S, \vee, \wedge, \preceq}\right)$ be a complete lattice.

Let $x, z \in S$.

Let $\mathcal R$ be an auxiliary approximating relation on $S$ such that

$\left({x, z}\right) \in \mathcal R \land x \ne z$


Then

$\exists y \in S: x \preceq y \land \left({y, z}\right) \in \mathcal R \land x \ne y$


Proof

By definition of auxiliary relation:

$x \preceq z$

By definition of $\prec$:

$x \prec z$

By definition of antisymmetry:

$z \nprec x$

Then

$z \npreceq x$

By Not Preceding implies Approximating Relation and not Preceding:

$\exists u \in S: \left({u, z}\right) \land u \npreceq x$

Define $y = x \vee u$.

Thus by Join Succeeds Operands:

$x \preceq y$

Thus by definition of auxiliary relation:

$\left({y, z}\right) \in \mathcal R$

Thus by Preceding iff Join equals Larger Operand:

$x \ne y$

$\blacksquare$


Sources