Weak Upper Closure in Restricted Ordering

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\struct {S, \preccurlyeq}$ be an ordered set.

Let $T \subseteq S$ be a subset of $S$.

Let $\preccurlyeq \restriction_T$ be the restricted ordering on $T$.


Then for all $t \in T$:

$t^{\succcurlyeq T} = T \cap t^{\succcurlyeq S}$

where:

$t^{\succcurlyeq T}$ is the weak upper closure of $t$ in $\struct {T, \preccurlyeq \restriction_T}$
$t^{\succcurlyeq S}$ is the weak upper closure of $t$ in $\struct {S, \preccurlyeq}$.


Proof

Let $t \in T$.

Suppose that:

$t' \in t^{\succcurlyeq T}$

By definition of weak upper closure $t^{\succcurlyeq T}$, this is equivalent to:

$t \preccurlyeq \restriction_T t'$

By definition of $\preccurlyeq \restriction_T$, this comes down to:

$t \preccurlyeq t' \land t' \in T$

as it is assumed that $t \in T$.


The first conjunct precisely expresses that $t' \in t^{\succcurlyeq S}$.

By definition of set intersection, it also holds that:

$t' \in T \cap t^{\succcurlyeq S}$

if and only if $t' \in T$ and $t' \in t^{\succcurlyeq S}$.


Thus it follows that the following are equivalent:

$t' \in t^{\succcurlyeq T}$
$t' \in T \cap t^{\succcurlyeq S}$

and hence the result follows, by definition of set equality.

$\blacksquare$