Upper Closure of Element without Element is Filter implies Element is Meet Irreducible

From ProofWiki
Jump to navigation Jump to search

Theorem

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

Let $x \in S$.

Let

$x^\succeq \setminus \left\{ {x}\right\}$ be a filter in $L$.


Then $x$ is meet irreducible.


Proof

Let $a, b \in S$.

Aiming for a contradiction suppose that

$x = a \wedge b$ and $x \ne a$ and $x \ne b$

By Meet Precedes Operands:

$x \preceq b$ and $x \preceq a$

By definition of upper closure of element:

$b, a \in x^\succeq$

By definitions of singleton and difference:

$b, a \in x^\succeq \setminus \left\{ {x}\right\}$

By definition of filtered:

$\exists z \in x^\succeq \setminus \left\{ {x}\right\}: z \preceq a \land z \preceq b$

By definition of infimum:

$z \preceq x$

By definition of upper set:

$x \in x^\succeq \setminus \left\{ {x}\right\}$

Thus this contradicts $x \in \left\{ {x}\right\}$ by definition of singleton.

$\blacksquare$


Sources