Ordered predicate

This file defines what it means for a tree map to be ordered. This definition is encoded in the Ordered predicate.

def Std.DTreeMap.Internal.Impl.Ordered {α : Type u} {β : α → Type v} [Ord α] (t : Impl α β) : Prop

Implementation detail of the tree map

Equations

• t.Ordered = List.Pairwise (fun (a b : (a : α) × β a) => compare a.fst b.fst = Ordering.lt) t.toListModel

Lemmas about the Ordered predicate

theorem Std.DTreeMap.Internal.Impl.Ordered.left {α : Type u} {β : α → Type v} [Ord α] {sz : Nat} {k : α} {v : β k} {l r : Impl α β} (h : (inner sz k v l r).Ordered) : l.Ordered

theorem Std.DTreeMap.Internal.Impl.Ordered.right {α : Type u} {β : α → Type v} [Ord α] {sz : Nat} {k : α} {v : β k} {l r : Impl α β} (h : (inner sz k v l r).Ordered) : r.Ordered

theorem Std.DTreeMap.Internal.Impl.Ordered.compare_left {α : Type u} {β : α → Type v} [Ord α] {sz : Nat} {k : α} {v : β k} {l r : Impl α β} (h : (inner sz k v l r).Ordered) {k' : (a : α) × β a} (hk' : k' ∈ l.toListModel) : compare k'.fst k = Ordering.lt

theorem Std.DTreeMap.Internal.Impl.Ordered.compare_left_beq_gt {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α → Ordering} [Internal.IsStrictCut compare k] {sz : Nat} {k' : α} {v' : β k'} {l r : Impl α β} (ho : (inner sz k' v' l r).Ordered) (hcmp : (k k').isGE = true) (p : (a : α) × β a) (hp : p ∈ l.toListModel) : (k p.fst == Ordering.gt) = true

theorem Std.DTreeMap.Internal.Impl.Ordered.compare_left_not_beq_eq {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α → Ordering} [Internal.IsStrictCut compare k] {sz : Nat} {k' : α} {v' : β k'} {l r : Impl α β} (ho : (inner sz k' v' l r).Ordered) (hcmp : (k k').isGE = true) (p : (a : α) × β a) (hp : p ∈ l.toListModel) : ¬(k p.fst == Ordering.eq) = true

theorem Std.DTreeMap.Internal.Impl.Ordered.compare_right {α : Type u} {β : α → Type v} [Ord α] {sz : Nat} {k : α} {v : β k} {l r : Impl α β} (h : (inner sz k v l r).Ordered) {k' : (a : α) × β a} (hk' : k' ∈ r.toListModel) : compare k k'.fst = Ordering.lt

theorem Std.DTreeMap.Internal.Impl.Ordered.compare_right_not_beq_gt {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α → Ordering} [Internal.IsStrictCut compare k] {sz : Nat} {k' : α} {v' : β k'} {l r : Impl α β} (ho : (inner sz k' v' l r).Ordered) (hcmp : (k k').isLE = true) (p : (a : α) × β a) (hp : p ∈ r.toListModel) : ¬(k p.fst == Ordering.gt) = true