Way Below iff Second Operand Preceding Supremum of Ideal implies First Operand is Element of Ideal

Theorem

Let $\mathscr S = \struct {S, \preceq}$ be an up-complete ordered set.

Let $x, y \in S$.

Then $x \ll y$ if and only if

$\forall I \in \map {\operatorname {Ids} } {\mathscr S}: y \preceq \sup I \implies x \in I$

where

$\ll$ denotes the way below relation,

$\map {\operatorname {Ids} } {\mathscr S}$ denotes the set of all ideals in $\mathscr S$.

Proof

Sufficient Condition

Let $x \ll y$

Let $I \in \map {\operatorname {Ids} } {\mathscr S}$ such that

$y \preceq \sup I$

By definition of ideal:

$I$ is directed and lower.

By definition of up-complete:

$I$ admits a supremum.

By definition of way below relation:

$\exists i \in I: x \preceq i$

Thus by definition of lower section:

$x \in I$

$\Box$

Necessary Condition

Assume that

$\forall I \in \map {\operatorname {Ids} } {\mathscr S}: y \preceq \sup I \implies x \in I$

Let $D$ be a directed subset of $S$ such that:

$D$ admits a supremum and $y \preceq \sup D$

By Supremum of Lower Closure of Set:

$D^\preceq$ admits a supremum and $\sup D^\preceq = \sup D$

where $D^\preceq$ denotes the lower closure of $D$.

By Lower Closure of Directed Subset is Ideal:

$D^\preceq$ is an ideal.

By assumption:

$x \in D^\preceq$

Thus by definition of lower closure of subset:

$\exists d \in D: x \preceq d$

Thus by definition of way below relation:

$x \ll y$

$\blacksquare$

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_3:20

• Mizar article WAYBEL_3:21