Not Preceding implies There Exists Meet Irreducible Element Not Preceding

From ProofWiki
Jump to navigation Jump to search


Let $L = \left({S, \vee, \wedge, \preceq}\right)$ be a bounded below continuous lattice.

Let $x, y \in S$ such that

$y \npreceq x$


$\exists p \in S: p$ is meet irreducible and $x \preceq p$ and $y \npreceq p$


By definition of continuous:

$L$ satisfies axiom of approximation


$\forall x \in S: x^\ll$ is directed.

By Axiom of Approximation in Up-Complete Semilattice

$\exists u \in S: u \ll y \land u \npreceq x$

By Way Below implies There Exists Way Below Open Filter Subset of Way Above Closure:

there exists way below open filter $F$ in $L$: $y \in F \subseteq u^\gg$

By Way Above Closure is Subset of Upper Closure of Element:

$u^\gg \subseteq u^\succeq$

By definition of upper set:

$x \notin F$

By definition of relative complement:

$x \in \complement_S\left({F}\right)$

By Upper Way Below Open Subset Complement is Non Empty implies There Exists Maximal Element of Complement:

$\exists m \in \complement_S\left({F}\right): x \preceq m \land m = \max \complement_S\left({F}\right)$

Thus by Maximal Element of Complement of Filter is Meet Irreducible:

$m$ is meet irreducible.


$x \preceq m$

Aiming for a contradiction suppose that

$y \preceq m$

By definition of upper set:

$m \in F$

This contradicts $m \in \complement_S\left({F}\right)$ by definition of greatest element.