Equivalence of Definitions of Principal Ideal of Preordered Set

Theorem

Let $\struct {S, \preceq}$ be a preordered set.

Let $I$ be an ideal in $S$.

The following definitions of the concept of Principal Ideal of Preordered Set are equivalent:

Definition 1

Then $I$ is a principal ideal if and only if:

$\exists x \in I: x$ is upper bound for $I$

Definition 2

Then $I$ is a principal ideal if and only if:

$\exists x \in S: I = x^\preceq$

where $x^\preceq$ denotes the lower closure of $x$.

Proof

Definition $1$ implies Definition $2$

Assume that

$\exists x \in I: x$ is upper bound for $I$

We will prove that

$I \subseteq x^\preceq$

Let $y \in I$.

By definition of upper bound:

$y \preceq x$

Thus by definition of lower closure of element:

$y \in x^\preceq$

$\Box$

We will prove that

$x^\preceq \subseteq I$

Let $y \in x^\preceq$.

By definition of lower closure of element:

$y \preceq x$

Thus by definition of lower section:

$y \in I$

$\Box$

Thus by definition of set equality:

$\exists x \in S: I = x^\preceq$

$\Box$

Definition $2$ implies Definition $1$

Assume that:

$\exists x \in S: I = x^\preceq$

By definition of reflexivity:

$x \preceq x$

Thus by definition of lower closure of element:

$x \in I$

Let $y \in I$.

Thus by definition of lower closure of element:

$y \preceq x$

$\blacksquare$

Sources

• Mizar article WAYBEL_0:48