Supremum of Lower Closure of Element
Jump to navigation
Jump to search
Theorem
Let $\struct {S, \preceq}$ be an ordered set.
Let $s$ be an element of $S$.
Then:
- $\map \sup {s^\preceq} = s$
where $s^\preceq$ denotes the lower closure of $s$.
Proof
\(\ds \map \sup {s^\preceq}\) | \(=\) | \(\ds \map \sup {\set s^\preceq}\) | Lower Closure of Singleton | |||||||||||
\(\ds \) | \(=\) | \(\ds \map \sup {\set s}\) | Supremum of Lower Closure of Set | |||||||||||
\(\ds \) | \(=\) | \(\ds s\) | Supremum of Singleton |
$\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_0:34