Composition of comparisons

This file defines the composition of two comparison results. In a linear order the comparison of a with c is constrained by the comparisons of a with b and of b with c: two lt compose to lt, eq is an identity, and lt followed by gt leaves the result open. Ordering.comp o₁ o₂ is the set of results compatible with o₁ followed by o₂, and compare_mem_comp shows that the actual comparison lies in it. In a dense linear order without endpoints the table is exact: every result it allows is realized by some intermediate point.

Main declarations

• Ordering.comp: the composition table on Ordering.
• Ordering.compare_mem_comp: compare a c lies in (compare a b).comp (compare b c).
• Ordering.exists_compare_eq_of_mem_comp: in a dense linear order without endpoints, a result in o₁.comp o₂ is realized through an intermediate point.

def Ordering.comp : Ordering → Ordering → Finset Ordering

The results of comparing a with c compatible with a comparing to b as o₁ and b to c as o₂, in a linear order.

Equations

• Ordering.lt.comp Ordering.lt = {Ordering.lt}
• Ordering.lt.comp Ordering.eq = {Ordering.lt}
• Ordering.lt.comp Ordering.gt = ⊤
• Ordering.eq.comp x✝ = {x✝}
• Ordering.gt.comp Ordering.lt = ⊤
• Ordering.gt.comp Ordering.eq = {Ordering.gt}
• Ordering.gt.comp Ordering.gt = {Ordering.gt}

@[simp]

theorem Ordering.eq_comp (o : Ordering) : eq.comp o = {o}

@[simp]

theorem Ordering.comp_eq (o : Ordering) : o.comp eq = {o}

theorem Ordering.compare_mem_comp {α : Type u_1} [LinearOrder α] (a b c : α) : compare a c ∈ (compare a b).comp (compare b c)

theorem Ordering.exists_compare_eq_of_mem_comp {α : Type u_1} [LinearOrder α] [DenselyOrdered α] [NoMinOrder α] [NoMaxOrder α] {a c : α} {o₁ o₂ : Ordering} (h : compare a c ∈ o₁.comp o₂) : ∃ (b : α), compare a b = o₁ ∧ compare b c = o₂

In a dense linear order without endpoints, every result the composition table allows is realized by some intermediate point.