upper set operation is a closure operator
In this entry, we shall prove the assertion made in
the main entry (http://planetmath.org/UpperSet) that ↑
is a closure operator. This will be done by checking
that the defining properties are satisfied. To begin,
recall the definition of our operation
:
Definition 1.
Let P be a poset and A a subset of P. The upper set of A is defined to be the set
↑A={b∈P∣(∃a∈A)a≤b} |
Now, we verify each of the properties which is required of a closure operator.
Theorem 1.
↑∅=∅
Proof.
Any statement of the form “(∃a∈∅)P(a)”
is identically false no matter what the predicate P (i.e. it is
an antitautology) and the set of objects satsfying an identically
false condition is empty, so ↑∅=∅.
∎
Theorem 2.
A⊆↑A
Proof.
This follows from reflexivity — for every a∈A, one has
a≤a, hence a∈↑A.
∎
Theorem 3.
↑↑A=↑A
Proof.
By the previous result, ↑A⊆↑↑A. Hence, it only remains to show that ↑↑A⊆↑A. This follows from transitivity. In order for some a to be an element of ↑↑A, there must exist b and c such that a≥b≥C and C∈A. By transitivity, A≥C, so a∈↑A, hence ↑↑A⊆↑A as well. ∎
Theorem 4.
If A and B are subsets of a partially ordered set, then
↑(A∪B)=(↑A)∪(↑B) |
Proof.
On the one hand, if a∈↑(A∪B), then a≥b for some b∈A∪B. It then follows that either b∈A or b∈B. In the former case, a∈↑A, in the latter case, a∈↑B so, either way a∈(↑A)∪(↑B). Hence ↑(A∪B)⊆(↑A)∪(↑B).
On the other hand, if a∈(↑A)∪(↑B), then either a∈(↑A) or a∈(↑B). In the former case, there exists b such that a≥b and b∈A. Since A⊆A∪B, we also have b∈A∪B, hence a∈↑(A∪B). Likewise, in the second case, we also conclude that a∈↑(A∪B). Therefore, we have (↑A)∪(↑B)⊆↑(A∪B). ∎
Theorem 5.
↑P=P
Theorem 6.
A⊆B, ↑A⊆↑B
Title | upper set operation is a closure operator |
---|---|
Canonical name | UpperSetOperationIsAClosureOperator |
Date of creation | 2013-03-22 16:41:43 |
Last modified on | 2013-03-22 16:41:43 |
Owner | rspuzio (6075) |
Last modified by | rspuzio (6075) |
Numerical id | 8 |
Author | rspuzio (6075) |
Entry type | Theorem![]() |
Classification | msc 06A06 |