Ordering


Definition

A binary relation \(\mathrel{R}\), on a set \(S\), is an ordering if and only if:

\(\mathrel{R}\) is reflexive:
\(\forall x \in S : x{\mathrel{R}}x\)
\(\mathrel{R}\) is transitive:
\(\forall x,y,z \in S : x{\mathrel{R}}y \wedge y{\mathrel{R}}z \Rightarrow x{\mathrel{R}}z\)
\(\mathrel{R}\) is anti-symmetric:
\(\forall x,y \in S : x{\mathrel{R}}y \wedge y{\mathrel{R}}x \Rightarrow x = y\)

Axioms

   order_refl: ?x ≤ ?x
  order_trans: ?x ≤ ?y \(\Longrightarrow\) ?y ≤ ?z
order_antisym: ?x ≤ ?y \(\Longrightarrow\) ?y ≤ ?x \(\Longrightarrow\) ?x = ?y
THEOREM    \(x \le x \sqcup y\)
sup_ge1: ?x ≤ ?x \(\sqcup\) ?y

Proof unavailable

THEOREM    \(y \le x \sqcup y\)
sup_ge2: ?y ≤ ?x \(\sqcup\) ?y

Proof unavailable

THEOREM   

A non-empty subset of an ordered set has one supremum at most.

Proof available

THEOREM   

A non-empty subset of an ordered set has one infimum at most.

Proof available

THEOREM   

An ordered set has one greatest element at most.

Proof available

THEOREM   

An ordered set has one smallest element at most.

Proof available

Proper supersets