# `Ordered` predicate #

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

source
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

Instances For

## Lemmas about the `Ordered` predicate #

source
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
source
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
source
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
source
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
source
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
source
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
source
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