Upper Closure of Singleton
Jump to navigation
Jump to search
Theorem
Let $\struct {S, \preceq}$ be an ordered set.
Let $s$ be an element of $S$.
Then:
- $\set s^\succeq = s^\succeq$
where:
- $\set s^\succeq$ denotes the upper closure of $\set s$
- $s^\succeq$ denotes the upper closure of $s$
Proof
\(\ds \set s^\succeq\) | \(=\) | \(\ds \bigcup \set {t^\succeq: t \in \set s}\) | Definition of Upper Closure of Subset | |||||||||||
\(\ds \) | \(=\) | \(\ds \bigcup \set {s^\succeq}\) | Definition of Singleton | |||||||||||
\(\ds \) | \(=\) | \(\ds s^\succeq\) | Union of Singleton |
$\blacksquare$
Sources
- Mizar article WAYBEL_0:def 18