Compact Closure is Intersection of Lower Closure and Compact Subset

Theorem

Let $L = \struct {S, \vee, \preceq}$ be a bounded below join semilattice.

Let $x \in S$.

Then $x^{\mathrm {compact} } = x^\preceq \cap \map K L$

where

$x^{\mathrm {compact} }$ denotes the compact closure of $x$,

$x^\preceq$ denotes the lower closure of $x$,

$\map K L$ denotes the compact subset of $L$.

$y \in x^{\mathrm {compact} }$

$y \preceq x$ and $y$ is compact by definition of compact closure

$y \in x^\preceq$ and $y$ is compact by definition of lower closure of element

$y \in x^\preceq$ and $y \in \map K L$ by definition of compact subset

$y \in x^\preceq \cap \map K L$ by definition of intersection

Hence the result, by definition of set equality.

$\blacksquare$