Finite Subset Bounds Element of Finite Suprema Set and Lower Closure

Theorem

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

Let $I$ be ideal in $L$.

Let $X$ be non empty finite subset of $S$.

Let $x \in S$ such that

$x \in \paren {\map {\operatorname {finsups} } {F \cup X} }^\preceq$

where

$\operatorname {finsups}$ denotes the finite suprema set

$X^\preceq$ denotes the lower closure of $X$.

Then there exists $a \in S$: $a \in I \land x \preceq a \vee \sup X$

Proof

This follows by mutatis mutandis of the proof of Finite Subset Bounds Element of Finite Infima Set and Upper Closure.

$\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_7:Lm2