Preceding is Top in Ordered Set of Auxiliary Relations

From ProofWiki
Jump to navigation Jump to search


Let $L = \left({S, \vee, \preceq}\right)$ be a bounded below join semilattice.

Let ${\it Aux}\left({L}\right)$ be the set of all auxiliary relations on $S$.

Let $P = \left({ {\it Aux}\left({L}\right), \precsim}\right)$ be an ordered set where $\precsim \mathop = \subseteq\restriction_{{\it Aux}\left({L}\right) \times {\it Aux}\left({L}\right)}$


$\preceq \mathop = \top_P$

where $\top_P$ denotes the greatest element in $P$.


By Preceding is Auxiliary Relation:

$\preceq \mathop \in {\it Aux}\left({L}\right)$

By definition

$\preceq$ is lower bound for $\varnothing$ in $P$

We will prove that

$\forall R \in {\it Aux}\left({L}\right): R$ is lower bound for $\varnothing \implies R \mathop \precsim \preceq$

Let $R \in {\it Aux}\left({L}\right)$

By condition $(i)$ of definition of auxiliary relation:

$R \mathop \subseteq \preceq$

Thus by definition of $\precsim$:

$R \mathop \precsim \preceq$


By definition of infimum:

$\preceq \mathop = \inf_P \varnothing$

Thus by Infimum of Empty Set is Greatest Element:

$\preceq \mathop = \top_P$