Interval orders

An interval order is an irreflexive relation r in which r a b and r c d imply r a d or r c b: no two r-related pairs are incomparable crosswise, so the order contains no copy of 2 + 2. Transitivity follows. Interval orders are the orders of precedence among intervals of a linear order, and the precedence of nonempty intervals is the motivating instance.

[UPSTREAM] candidate for mathlib's order theory.

Main definitions

• IsIntervalOrder α r: r is an interval order on α.

Main results

• IsIntervalOrder.toIsStrictOrder: an interval order is a strict order.
• IsIntervalOrder.invImage: interval orders pull back along maps.
• NonemptyInterval.isIntervalOrder_precedes: precedence of intervals in a linear order.

References

• [Fis70]

class IsIntervalOrder (α : Sort u_1) (r : α → α → Prop) extends Std.Irrefl r : Prop

An interval order: an irreflexive relation in which r a b and r c d imply r a d or r c b.

• irrefl (a : α) : ¬r a a
• two_plus_two ⦃a b c d : α⦄ : r a b → r c d → r a d ∨ r c b

  Two related pairs are related crosswise in one direction.

@[instance 100]

instance IsIntervalOrder.toIsStrictOrder {α : Sort u_1} {r : α → α → Prop} [IsIntervalOrder α r] : IsStrictOrder α r

theorem IsIntervalOrder.invImage {α : Sort u_1} {β : Sort u_2} {r : α → α → Prop} (h : IsIntervalOrder α r) (f : β → α) : IsIntervalOrder β (InvImage r f)

An interval order pulls back along any map.

instance NonemptyInterval.isIntervalOrder_precedes {α : Type u_1} [LinearOrder α] : IsIntervalOrder (NonemptyInterval α) Precedes

Precedence of intervals in a linear order is an interval order.