Ordered predicate #
This file defines what it means for a tree map to be ordered. This definition is encoded in the
Ordered predicate.
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
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)
:
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)
:
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)
:
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)
:
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)
: