# Completely Irreducible Element equals Infimum of Subset implies Element Belongs to Subset

Jump to navigation
Jump to search

## Theorem

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

Let $X \subseteq S$, $p \in S$ such that

- $p$ is completely irreducible and $p = \inf X$

Then $p \in X$

## Proof

Aiming for a contradiction, suppose

- $p \notin X$

By Completely Irreducible Element iff Exists Element that Strictly Succeeds First Element:

- $\exists q \in S: p \prec q \land \left({\forall s \in S: p \prec s \implies q \preceq s}\right) \land p^\succeq = \left\{ {p}\right\} \cup q^\succeq$

where $p^\succeq$ denotes the upper closure of $p$.

We will prove that

- $q$ is lower bound for $X$

Let $x \in X$.

By definitions of infimum and lower bound

- $p \preceq x$

By assumption:

- $x \ne p$

By definition of strictly precede:

- $p \prec x$

Thus by step condition:

- $q \preceq x$

$\Box$

By definition of strictly precede:

- $p \preceq q$

We will prove that

- $\forall b \in S: b$ is lower bound for $X \implies b \preceq q$

Let $b \in S$ such that

- $b$ is lower bound for $X$.

By definition of infimum:

- $b \preceq p$

Thus by definition of transitivity:

- $b \preceq q$

$\Box$

By definition of infimum:

- $q = \inf X = p$

Thus this contradicts $p \ne q$ by definition of strictly precede.

$\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 WAYBEL16:34