Characterization of Prime Element in Meet Semilattice
Theorem
Let $L = \struct {S, \wedge, \preceq}$ be a meet semilattice.
Let $p \in S$,
Then:
- $p$ is prime element
- for all non-empty finite subsets $A$ of $S$:
- if $\inf A \preceq p$, then there exists element $x$ of $A$ such that $x \preceq p$.
Proof
Sufficient Condition
Let $p$ be prime element.
Let $A$ be non-empty finite subsets of $S$.
Define
- $\map P X : \equiv X \ne \O \land \inf X \preceq p \implies \exists x \in X: x \preceq p$
where $X \subseteq S$.
We will prove that
- $\forall x \in A, B \subseteq A: \map P B \implies \map P {B \cup \set x}$
Let $x \in A, B \subseteq A$ such that
- $\map P B$
and
- $B \cup \set x \ne \O$ and $\map \inf {B \cup \set x} \preceq p$
Case $B = \O$.
- $B \cup \set x = \set x$
- $\inf \set x = x$
By definition of singleton:
- $x \in \set x$
Thus
- $\exists z \in B \cup \set x: z \preceq p$
$\Box$
Case $B \ne \O$.
By Subset of Finite Set is Finite:
- $B$ is finite.
By Existence of Non-Empty Finite Infima in Meet Semilattice:
- $B, \set x$ admit infima.
- $\map \inf {B \cup \set x} = \inf B \wedge \inf \set x$
By definition of prime element:
- $\inf B \preceq p$ or $x \preceq p$
Case $\inf B \preceq p$.
By assumption:
- $\exists z \in B: z \preceq p$
By definition of union:
- $z \in B \cup \set x$
Thus
- $\exists z \in B \cup \set x: z \preceq p$
$\Box$
Case $x \preceq p$.
By definitions of union and singleton:
- $x \in B \cup \set x$
Thus
- $\exists z \in B \cup \set x: z \preceq p$
$\Box$
By definition of empty set:
- $\map P \O$
- $\map P A$
Thus
- if $\inf A \preceq p$, then there exists element $x$ of $A$ such that $x \preceq p$.
$\Box$
Necessary Condition
Suppose that
- for all non-empty finite subsets $A$ of $S$:
- if $\inf A \preceq p$, then there exists element $x$ of $A$ such that $x \preceq p$.
Let $x, y \in S$ such that
- $x \wedge y \preceq p$
Define $A := \set {x, y}$
By definitions of non-empty set and finite set:
By definition of meet:
- $\inf A = x \wedge y$
By assumption:
- $\exists z \in A: z \preceq p$
Thus by definition of unordered tuple:
- $x \preceq p$ or $y \preceq p$
$\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_6:22