Left-linear orders

A partial order is left-linear when the predecessors of every element are linearly ordered: a ≤ c → b ≤ c → a ≤ b ∨ b ≤ a. Equivalently, every principal down-set Iic m is a chain. This is the order-theoretic notion of a tree: the order may branch upward but never downward.

Left-linearity is the shared kernel of two linglib substrates: the Connected Ancestor Condition of [BP90] syntactic trees (Core.Order.TreeOrder) and the no-backward-branching axiom of Prior–Thomason branching time. Both consume IsLeftLinear; "ancestors are linearly ordered" (c-command) and "the past is linear" (branching time) are literally the same statement, IsLeftLinear.isChain_Iio.

Main definitions

• IsLeftLinear M — the predecessors of every element are linearly ordered.

Main results

• IsLeftLinear.isChain_Iic, IsLeftLinear.isChain_Iio — every principal down-set is a chain.

class IsLeftLinear (M : Type u_1) [PartialOrder M] : Prop

A partial order is left-linear when the predecessors of every element are linearly ordered (no backward branching). The order-theoretic notion of a tree order.

• comparable_of_le_common ⦃a b c : M⦄ : a ≤ c → b ≤ c → a ≤ b ∨ b ≤ a

  The predecessors of any element are pairwise comparable.

theorem IsLeftLinear.isChain_Iic {M : Type u_1} [PartialOrder M] [IsLeftLinear M] (m : M) : IsChain (fun (x1 x2 : M) => x1 ≤ x2) (Set.Iic m)

In a left-linear order the principal down-set Iic m is a chain.

theorem IsLeftLinear.isChain_Iio {M : Type u_1} [PartialOrder M] [IsLeftLinear M] (m : M) : IsChain (fun (x1 x2 : M) => x1 ≤ x2) (Set.Iio m)

In a left-linear order the strict past Iio m is a chain: the predecessors of any moment are linearly ordered.