# Equivalence of Definitions of Principal Ideal

Jump to navigation
Jump to search

This page has been identified as a candidate for refactoring.standard equivalence proof formUntil this has been finished, please leave
`{{Refactor}}` in the code.
Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$.To discuss this page in more detail, feel free to use the talk page.When this work has been completed, you may remove this instance of `{{Refactor}}` from the code. |

## Theorem

Let $\left({S, \preceq}\right)$ be a preordered set.

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

Then

- the definitions of principal ideal are equivalent,

That means that

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

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

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

## Proof

### Sufficient Condition

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 set:

- $y \in I$

$\Box$

Thus by definition of set equality:

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

$\Box$

### Necessary Condition

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