Supremum in Ordered Subset
Jump to navigation
Jump to search
Theorem
Let $L = \struct {S, \preceq}$ be an ordered set.
Let $R = \struct {T, \preceq'}$ be an ordered subset of $L$.
Let $X \subseteq T$ such that
- $X$ admits an supremum in $L$.
Then $\sup_L X \in T$ if and only if
- $X$ admits an supremum in $R$ and $\sup_R X = \sup_L X$
Proof
This follows by mutatis mutandis of the proof of Infimum in Ordered Subset.
$\blacksquare$
Sources
- Mizar article YELLOW_0:64