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.

Linear orders are left-linear, and so is every rooted tree in the sense of Mathlib/Order/SuccPred/Tree.lean: a PredOrder with archimedean predecessor is left-linear by mathlib's le_total_of_directed. Left-linearity also pulls back along any order embedding (OrderEmbedding.isLeftLinear), so a suborder of a tree is left-linear. Branching-time frames, which need not have predecessors, assume left-linearity directly.

The flags of a left-linear order, mathlib's maximal chains, behave like the branches of a tree: a flag through an element contains its entire past (Flag.Iic_subset), the down-set of a maximal element is a flag (Flag.ofIsMax), and on a finite order every flag arises this way (Flag.exists_isMax_eq_ofIsMax), which turns quantification over flags into quantification over maximal elements (Flag.forall_mem_iff) and so makes it decidable.

Main definitions

• IsLeftLinear M: the predecessors of every element are linearly ordered.
• Flag.ofIsMax: the down-set of a maximal element, as a flag.

Main results

• IsLeftLinear.isChain_Iic: every principal down-set is a chain.
• Flag.exists_mem_gt_of_lt: a flag cannot stop at an element with a strict successor; this holds in any order.
• Flag.exists_isMax_eq_ofIsMax, Flag.forall_mem_iff: on a finite left-linear order the flags are the down-sets of the maximal elements.

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

A partial order is left-linear when the predecessors of every element are linearly ordered, so that it never branches backward.

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

  The predecessors of any element are pairwise comparable.

@[instance 100]

instance instIsLeftLinear {M : Type u_1} [LinearOrder M] : IsLeftLinear M

A linear order is left-linear.

@[instance 100]

instance instIsLeftLinearOfIsPredArchimedean {M : Type u_1} [PartialOrder M] [PredOrder M] [IsPredArchimedean M] : IsLeftLinear M

A PredOrder with archimedean predecessor, such as a rooted tree, is left-linear.

theorem OrderEmbedding.isLeftLinear {M : Type u_1} {N : Type u_2} [PartialOrder M] [PartialOrder N] [IsLeftLinear N] (f : M ↪o N) : IsLeftLinear M

Left-linearity pulls back along an order embedding.

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.le_of_lt_of_covBy {M : Type u_1} [PartialOrder M] [IsLeftLinear M] {a b m : M} (hm : m ⋖ a) (hb : b < a) : b ≤ m

In a left-linear order everything strictly below an element is below the element it covers, its mother in a tree.

Flags

In a left-linear order a flag, mathlib's maximal chain, is a branch: it contains the whole past of each of its elements, and when the order is finite it is the down-set of a maximal element.

@[instance_reducible]

instance instDecidableIsMaxOfFintypeOfDecidableLE_linglib {M : Type u_1} [PartialOrder M] [Fintype M] [DecidableLE M] (x : M) : Decidable (IsMax x)

Maximality is decidable on a finite type.

Equations

• instDecidableIsMaxOfFintypeOfDecidableLE_linglib x = decidable_of_iff (∀ (b : M), x ≤ b → b ≤ x) ⋯

theorem Flag.exists_mem_gt_of_lt {M : Type u_1} [PartialOrder M] {m x : M} {h : Flag M} (hm : m ∈ h) (hx : m < x) : ∃ y ∈ h, m < y

A flag through a non-maximal element contains a strictly larger one; otherwise inserting the successor would extend the chain.

theorem Flag.Iic_subset {M : Type u_1} [PartialOrder M] {m : M} {h : Flag M} [IsLeftLinear M] (hm : m ∈ h) : Set.Iic m ⊆ ↑h

In a left-linear order a flag contains the entire past of each of its elements.

def Flag.ofIsMax {M : Type u_1} [PartialOrder M] {x : M} [IsLeftLinear M] (hx : IsMax x) : Flag M

The down-set of a maximal element of a left-linear order, as a flag.

Equations

• Flag.ofIsMax hx = { carrier := Set.Iic x, Chain' := ⋯, max_chain' := ⋯ }

@[simp]

theorem Flag.mem_ofIsMax {M : Type u_1} [PartialOrder M] {x y : M} [IsLeftLinear M] {hx : IsMax x} : y ∈ ofIsMax hx ↔ y ≤ x

theorem Flag.eq_ofIsMax_of_mem {M : Type u_1} [PartialOrder M] {x : M} {h : Flag M} [IsLeftLinear M] (hx : IsMax x) (hxh : x ∈ h) : h = ofIsMax hx

A flag through a maximal element is its down-set.

theorem Flag.exists_isMax_eq_ofIsMax {M : Type u_1} [PartialOrder M] [IsLeftLinear M] [Finite M] [Nonempty M] (h : Flag M) : ∃ (x : M) (hx : IsMax x), h = ofIsMax hx

On a finite left-linear order every flag is the down-set of a maximal element, since the flag has a greatest element, which a strict successor would contradict.

theorem Flag.forall_mem_iff {M : Type u_1} [PartialOrder M] {m : M} [IsLeftLinear M] [Finite M] [Nonempty M] {P : Flag M → Prop} : (∀ (h : Flag M), m ∈ h → P h) ↔ ∀ (x : M) (hx : IsMax x), m ≤ x → P (ofIsMax hx)

On a finite left-linear order, quantifying over the flags through an element is quantifying over the maximal elements above it.