Infimum of Upper Closure of Set
Jump to navigation
Jump to search
Theorem
Let $\left({S, \preceq}\right)$ be an ordered set.
Let $T \subseteq S$.
Let $U = T^\succeq$ be the upper closure of $T$ in $S$.
Let $s \in S$.
Then $s$ is the infimum of $T$ if and only if it is the infimum of $U$.
Proof
This follows by mutatis mutandis of the proof of Supremum of Lower Closure of Set.
$\blacksquare$
Sources
- Mizar article WAYBEL_0:37
- Mizar article WAYBEL_0:38