Ordered sets

Partial, strict and total orders, dense linear orders, monotone maps and sequences, and representations of finite posets.

• Monotone sequences
• Strict total orders

DefinitionDense linear order without endpoints#✓fully proved

A relation \(R\) on a type \(\alpha\) is a dense linear order without endpoints if it is a strict total order (irreflexive, transitive, and trichotomous: for all \(a, b\), at least one of \(R(a,b)\), \(a = b\), \(R(b,a)\) holds), it is dense (whenever \(R(a,b)\), there is \(c\) with \(R(a,c)\) and \(R(c,b)\)), and it has no endpoints (for every \(a\) there are \(b\) and \(b'\) with \(R(b,a)\) and \(R(a,b')\)).

def IsDenseLinearOrderWithoutEndpoints {α : Type*} (r : α → α → Prop) : Prop :=
   IsStrictTotalOrder α r ∧
   (∀ a b, r a b → ∃ c, r a c ∧ r c b) ∧
   (∀ a, ∃ b, r b a) ∧
   (∀ a, ∃ b, r a b)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.