Strict Upper Closure in Restricted Ordering
Theorem
Let $\struct {S, \preceq}$ be an ordered set.
Let $T \subseteq S$ be a subset of $S$, and let $\preceq \restriction_T$ be the restricted ordering on $T$.
Then for all $t \in T$:
- $t^{\succ T} = T \cap t^{\succ S}$
where:
- $t^{\succ T}$ is the strict upper closure of $t$ in $\struct {T, \preceq \restriction_T}$
- $t^{\succ S}$ is the strict upper closure of $t$ in $\struct {S, \preceq}$.
Proof
Let $t \in T$, and suppose that $t' \in t^{\succ T}$.
By definition of strict upper closure, this is equivalent to:
- $t \preceq \restriction_T t' \land t \ne t'$
By definition of $\preceq \restriction_T$, the first condition comes down to:
- $t \preceq t' \land t' \in T$
as it is assumed that $t \in T$.
In conclusion, $t' \in t^{\succ T}$ is equivalent to:
- $t' \in T \land t \preceq t' \land t \ne t'$
These last two conjuncts precisely express that $t' \in t^{\succ S}$.
By definition of set intersection, it also holds that:
- $t' \in T \cap t^{\succ S}$
if and only if $t' \in T$ and $t' \in t^{\succ S}$.
Thus, it follows that the following are equivalent:
- $t' \in t^{\succ T}$
- $t' \in T \cap t^{\succ S}$
and hence the result follows, by definition of set equality.
$\blacksquare$