Maximal implies Completely Irreducible

From ProofWiki
Jump to navigation Jump to search

Theorem

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

Let $p \in S$ such that

$\exists k \in S: p$ is maximal in $S \setminus k^\succeq$


Then $p$ is completely irreducible.


Proof

By Join Succeeds Operands:

$k \preceq p \vee k$ and $p \preceq p \vee k$

By definition of upper closure of element:

$p \vee k \in k^\succeq$ and $p \vee k \in p^\succeq$

By definition of intersection:

$p \vee k \in p^\succeq \cap k^\succeq$

By Maximal implies Difference equals Intersection:

$p^\succeq \setminus \set p = p^\succeq \cap k^\succeq$

By Infimum of Intersection of Upper Closures equals Join Operands

$\map \inf {p^\succeq \cap k^\succeq} = p \vee k$

By definition:

$p^\succeq \setminus \set p$ admits a minimum.

Thus by definition:

$p$ is completely irreducible.

$\blacksquare$


Sources