Upper Closure of Element is Way Below Open Filter iff Element is Compact

Theorem

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

Let $x \in S$.

Then:

$x^\succeq$ is a way below open filter on $L$

if and only if

$x$ is compact

Proof

Sufficient Condition

Suppose:

$x^\succeq$ is a way below open filter on $L$

By definitions of upper closure of element and reflexivity:

$x \in x^\succeq$

By definition of way below open:

$\exists y \in x^\succeq: y \ll x$

By definition of upper closure of element:

$x \preceq y$

By Preceding and Way Below implies Way Below and definition of reflexivity:

$x \ll x$

By definition:

$x$ is compact.

$\Box$

Necessary Condition

Let $x$ be compact.

By Upper Closure of Element is Filter:

$x^\succeq$ is filter on $L$.

It remains to show that:

$x^\succeq$ is way below open.

Let $u \in x^\succeq$.

By definition of upper closure of element:

$x \preceq u$

and by definition of reflexivity:

$x \in x^\succeq$

By definition of compact:

$x \ll x$

By Preceding and Way Below implies Way Below:

$x \ll u$

Thus

$\exists z \in x^\succeq: z \ll u$

$\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_8:2