Filter is Ideal in Dual Ordered Set
Jump to navigation
Jump to search
Theorem
Let $P = \struct {S, \preceq}$ be an ordered set.
Let $X$ be a subset of $S$.
Then
- $X$ is filter in $P$
- $X$ is ideal in $P^{-1}$
where $P^{-1} = \struct {S, \succeq}$ denotes the dual of $P$.
Proof
- dual of $P^{-1}$ is $P$.
Hence by Ideal is Filter in Dual Ordered Set:
- the result fallows.
$\blacksquare$
Sources
- Mizar article YELLOW_7:29
- Mizar article YELLOW_7:27