Documentation

Mathlib.Data.Ordmap.Invariants

Invariants for the verification of Ordnode #

An Ordnode, defined in Mathlib.Data.Ordmap.Ordnode, is an inductive type which describes a tree which stores the size at internal nodes.

In this file we define the correctness invariant of an Ordnode, comprising:

This whole file is in the Ordnode namespace, because we first have to prove the correctness of all the operations (and defining what correctness means here is somewhat subtle). The actual Ordset operations are in Mathlib.Data.Ordmap.Ordset.

TODO #

This file is incomplete, in the sense that the intent is to have verified versions and lemmas about all the definitions in Ordnode.lean, but at the moment only a few operations are verified (the hard part should be out of the way, but still). Contributors are encouraged to pick this up and finish the job, if it appeals to you.

Tags #

ordered map, ordered set, data structure, verified programming

delta and ratio #

theorem Ordnode.not_le_delta {s : } (H : 1 s) :
theorem Ordnode.delta_lt_false {a b : } (h₁ : delta * a < b) (h₂ : delta * b < a) :

singleton #

size and empty #

def Ordnode.realSize {α : Type u_1} :
Ordnode α

O(n). Computes the actual number of elements in the set, ignoring the cached size field.

Equations
Instances For

    Sized #

    def Ordnode.Sized {α : Type u_1} :
    Ordnode αProp

    The Sized property asserts that all the size fields in nodes match the actual size of the respective subtrees.

    Equations
    Instances For
      theorem Ordnode.Sized.node' {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : l.Sized) (hr : r.Sized) :
      (l.node' x r).Sized
      theorem Ordnode.Sized.eq_node' {α : Type u_1} {s : } {l : Ordnode α} {x : α} {r : Ordnode α} (h : (node s l x r).Sized) :
      node s l x r = l.node' x r
      theorem Ordnode.Sized.size_eq {α : Type u_1} {s : } {l : Ordnode α} {x : α} {r : Ordnode α} (H : (node s l x r).Sized) :
      (node s l x r).size = l.size + r.size + 1
      theorem Ordnode.Sized.induction {α : Type u_1} {t : Ordnode α} (hl : t.Sized) {C : Ordnode αProp} (H0 : C nil) (H1 : ∀ (l : Ordnode α) (x : α) (r : Ordnode α), C lC rC (l.node' x r)) :
      C t
      theorem Ordnode.size_eq_realSize {α : Type u_1} {t : Ordnode α} :
      t.Sizedt.size = t.realSize
      @[simp]
      theorem Ordnode.Sized.size_eq_zero {α : Type u_1} {t : Ordnode α} (ht : t.Sized) :
      t.size = 0 t = nil
      theorem Ordnode.Sized.pos {α : Type u_1} {s : } {l : Ordnode α} {x : α} {r : Ordnode α} (h : (node s l x r).Sized) :
      0 < s

      dual

      theorem Ordnode.dual_dual {α : Type u_1} (t : Ordnode α) :
      t.dual.dual = t
      @[simp]
      theorem Ordnode.size_dual {α : Type u_1} (t : Ordnode α) :

      Balanced

      The BalancedSz l r asserts that a hypothetical tree with children of sizes l and r is balanced: either l ≤ δ * r and r ≤ δ * r, or the tree is trivial with a singleton on one side and nothing on the other.

      Equations
      Instances For
        def Ordnode.Balanced {α : Type u_1} :
        Ordnode αProp

        The Balanced t asserts that the tree t satisfies the balance invariants (at every level).

        Equations
        Instances For
          theorem Ordnode.balancedSz_up {l r₁ r₂ : } (h₁ : r₁ r₂) (h₂ : l + r₂ 1 r₂ delta * l) (H : BalancedSz l r₁) :
          BalancedSz l r₂
          theorem Ordnode.balancedSz_down {l r₁ r₂ : } (h₁ : r₁ r₂) (h₂ : l + r₂ 1 l delta * r₁) (H : BalancedSz l r₂) :
          BalancedSz l r₁
          theorem Ordnode.Balanced.dual {α : Type u_1} {t : Ordnode α} :

          rotate and balance #

          def Ordnode.node3L {α : Type u_1} (l : Ordnode α) (x : α) (m : Ordnode α) (y : α) (r : Ordnode α) :

          Build a tree from three nodes, left associated (ignores the invariants).

          Equations
          Instances For
            def Ordnode.node3R {α : Type u_1} (l : Ordnode α) (x : α) (m : Ordnode α) (y : α) (r : Ordnode α) :

            Build a tree from three nodes, right associated (ignores the invariants).

            Equations
            Instances For
              def Ordnode.node4L {α : Type u_1} :
              Ordnode ααOrdnode ααOrdnode αOrdnode α

              Build a tree from three nodes, with a () b -> (a ()) b and a (b c) d -> ((a b) (c d)).

              Equations
              Instances For
                def Ordnode.node4R {α : Type u_1} :
                Ordnode ααOrdnode ααOrdnode αOrdnode α

                Build a tree from three nodes, with a () b -> a (() b) and a (b c) d -> ((a b) (c d)).

                Equations
                Instances For
                  def Ordnode.rotateL {α : Type u_1} :
                  Ordnode ααOrdnode αOrdnode α

                  Concatenate two nodes, performing a left rotation x (y z) -> ((x y) z) if balance is upset.

                  Equations
                  Instances For
                    theorem Ordnode.rotateL_node {α : Type u_1} (l : Ordnode α) (x : α) (sz : ) (m : Ordnode α) (y : α) (r : Ordnode α) :
                    l.rotateL x (node sz m y r) = if m.size < ratio * r.size then l.node3L x m y r else l.node4L x m y r
                    theorem Ordnode.rotateL_nil {α : Type u_1} (l : Ordnode α) (x : α) :
                    def Ordnode.rotateR {α : Type u_1} :
                    Ordnode ααOrdnode αOrdnode α

                    Concatenate two nodes, performing a right rotation (x y) z -> (x (y z)) if balance is upset.

                    Equations
                    Instances For
                      theorem Ordnode.rotateR_node {α : Type u_1} (sz : ) (l : Ordnode α) (x : α) (m : Ordnode α) (y : α) (r : Ordnode α) :
                      (node sz l x m).rotateR y r = if m.size < ratio * l.size then l.node3R x m y r else l.node4R x m y r
                      theorem Ordnode.rotateR_nil {α : Type u_1} (y : α) (r : Ordnode α) :
                      def Ordnode.balanceL' {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α) :

                      A left balance operation. This will rebalance a concatenation, assuming the original nodes are not too far from balanced.

                      Equations
                      Instances For
                        def Ordnode.balanceR' {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α) :

                        A right balance operation. This will rebalance a concatenation, assuming the original nodes are not too far from balanced.

                        Equations
                        Instances For
                          def Ordnode.balance' {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α) :

                          The full balance operation. This is the same as balance, but with less manual inlining. It is somewhat easier to work with this version in proofs.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            theorem Ordnode.dual_node' {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α) :
                            (l.node' x r).dual = r.dual.node' x l.dual
                            theorem Ordnode.dual_node3L {α : Type u_1} (l : Ordnode α) (x : α) (m : Ordnode α) (y : α) (r : Ordnode α) :
                            (l.node3L x m y r).dual = r.dual.node3R y m.dual x l.dual
                            theorem Ordnode.dual_node3R {α : Type u_1} (l : Ordnode α) (x : α) (m : Ordnode α) (y : α) (r : Ordnode α) :
                            (l.node3R x m y r).dual = r.dual.node3L y m.dual x l.dual
                            theorem Ordnode.dual_node4L {α : Type u_1} (l : Ordnode α) (x : α) (m : Ordnode α) (y : α) (r : Ordnode α) :
                            (l.node4L x m y r).dual = r.dual.node4R y m.dual x l.dual
                            theorem Ordnode.dual_node4R {α : Type u_1} (l : Ordnode α) (x : α) (m : Ordnode α) (y : α) (r : Ordnode α) :
                            (l.node4R x m y r).dual = r.dual.node4L y m.dual x l.dual
                            theorem Ordnode.dual_rotateL {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α) :
                            (l.rotateL x r).dual = r.dual.rotateR x l.dual
                            theorem Ordnode.dual_rotateR {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α) :
                            (l.rotateR x r).dual = r.dual.rotateL x l.dual
                            theorem Ordnode.dual_balance' {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α) :
                            theorem Ordnode.dual_balanceL {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α) :
                            theorem Ordnode.dual_balanceR {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α) :
                            theorem Ordnode.Sized.node3L {α : Type u_1} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} (hl : l.Sized) (hm : m.Sized) (hr : r.Sized) :
                            (l.node3L x m y r).Sized
                            theorem Ordnode.Sized.node3R {α : Type u_1} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} (hl : l.Sized) (hm : m.Sized) (hr : r.Sized) :
                            (l.node3R x m y r).Sized
                            theorem Ordnode.Sized.node4L {α : Type u_1} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} (hl : l.Sized) (hm : m.Sized) (hr : r.Sized) :
                            (l.node4L x m y r).Sized
                            theorem Ordnode.node3L_size {α : Type u_1} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} :
                            (l.node3L x m y r).size = l.size + m.size + r.size + 2
                            theorem Ordnode.node3R_size {α : Type u_1} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} :
                            (l.node3R x m y r).size = l.size + m.size + r.size + 2
                            theorem Ordnode.node4L_size {α : Type u_1} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} (hm : m.Sized) :
                            (l.node4L x m y r).size = l.size + m.size + r.size + 2
                            theorem Ordnode.Sized.dual {α : Type u_1} {t : Ordnode α} :
                            t.Sizedt.dual.Sized
                            theorem Ordnode.Sized.dual_iff {α : Type u_1} {t : Ordnode α} :
                            theorem Ordnode.Sized.rotateL {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : l.Sized) (hr : r.Sized) :
                            (l.rotateL x r).Sized
                            theorem Ordnode.Sized.rotateR {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : l.Sized) (hr : r.Sized) :
                            (l.rotateR x r).Sized
                            theorem Ordnode.Sized.rotateL_size {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (hm : r.Sized) :
                            (l.rotateL x r).size = l.size + r.size + 1
                            theorem Ordnode.Sized.rotateR_size {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : l.Sized) :
                            (l.rotateR x r).size = l.size + r.size + 1
                            theorem Ordnode.Sized.balance' {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : l.Sized) (hr : r.Sized) :
                            (l.balance' x r).Sized
                            theorem Ordnode.size_balance' {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : l.Sized) (hr : r.Sized) :
                            (l.balance' x r).size = l.size + r.size + 1

                            All, Any, Emem, Amem #

                            theorem Ordnode.All.imp {α : Type u_1} {P Q : αProp} (H : ∀ (a : α), P aQ a) {t : Ordnode α} :
                            All P tAll Q t
                            theorem Ordnode.Any.imp {α : Type u_1} {P Q : αProp} (H : ∀ (a : α), P aQ a) {t : Ordnode α} :
                            Any P tAny Q t
                            theorem Ordnode.all_singleton {α : Type u_1} {P : αProp} {x : α} :
                            All P {x} P x
                            theorem Ordnode.any_singleton {α : Type u_1} {P : αProp} {x : α} :
                            Any P {x} P x
                            theorem Ordnode.all_dual {α : Type u_1} {P : αProp} {t : Ordnode α} :
                            All P t.dual All P t
                            theorem Ordnode.all_iff_forall {α : Type u_1} {P : αProp} {t : Ordnode α} :
                            All P t ∀ (x : α), Emem x tP x
                            theorem Ordnode.any_iff_exists {α : Type u_1} {P : αProp} {t : Ordnode α} :
                            Any P t ∃ (x : α), Emem x t P x
                            theorem Ordnode.emem_iff_all {α : Type u_1} {x : α} {t : Ordnode α} :
                            Emem x t ∀ (P : αProp), All P tP x
                            theorem Ordnode.all_node' {α : Type u_1} {P : αProp} {l : Ordnode α} {x : α} {r : Ordnode α} :
                            All P (l.node' x r) All P l P x All P r
                            theorem Ordnode.all_node3L {α : Type u_1} {P : αProp} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} :
                            All P (l.node3L x m y r) All P l P x All P m P y All P r
                            theorem Ordnode.all_node3R {α : Type u_1} {P : αProp} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} :
                            All P (l.node3R x m y r) All P l P x All P m P y All P r
                            theorem Ordnode.all_node4L {α : Type u_1} {P : αProp} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} :
                            All P (l.node4L x m y r) All P l P x All P m P y All P r
                            theorem Ordnode.all_node4R {α : Type u_1} {P : αProp} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} :
                            All P (l.node4R x m y r) All P l P x All P m P y All P r
                            theorem Ordnode.all_rotateL {α : Type u_1} {P : αProp} {l : Ordnode α} {x : α} {r : Ordnode α} :
                            All P (l.rotateL x r) All P l P x All P r
                            theorem Ordnode.all_rotateR {α : Type u_1} {P : αProp} {l : Ordnode α} {x : α} {r : Ordnode α} :
                            All P (l.rotateR x r) All P l P x All P r
                            theorem Ordnode.all_balance' {α : Type u_1} {P : αProp} {l : Ordnode α} {x : α} {r : Ordnode α} :
                            All P (l.balance' x r) All P l P x All P r

                            toList #

                            theorem Ordnode.foldr_cons_eq_toList {α : Type u_1} (t : Ordnode α) (r : List α) :
                            @[simp]
                            theorem Ordnode.toList_nil {α : Type u_1} :
                            @[simp]
                            theorem Ordnode.toList_node {α : Type u_1} (s : ) (l : Ordnode α) (x : α) (r : Ordnode α) :
                            (node s l x r).toList = l.toList ++ x :: r.toList
                            theorem Ordnode.emem_iff_mem_toList {α : Type u_1} {x : α} {t : Ordnode α} :
                            Emem x t x t.toList
                            theorem Ordnode.length_toList {α : Type u_1} {t : Ordnode α} (h : t.Sized) :
                            theorem Ordnode.equiv_iff {α : Type u_1} {t₁ t₂ : Ordnode α} (h₁ : t₁.Sized) (h₂ : t₂.Sized) :
                            t₁.Equiv t₂ t₁.toList = t₂.toList

                            mem #

                            theorem Ordnode.pos_size_of_mem {α : Type u_1} [LE α] [DecidableLE α] {x : α} {t : Ordnode α} (h : t.Sized) (h_mem : x t) :
                            0 < t.size

                            (find/erase/split)(Min/Max) #

                            theorem Ordnode.findMin'_dual {α : Type u_1} (t : Ordnode α) (x : α) :
                            theorem Ordnode.findMax'_dual {α : Type u_1} (t : Ordnode α) (x : α) :
                            theorem Ordnode.findMin_dual {α : Type u_1} (t : Ordnode α) :
                            theorem Ordnode.findMax_dual {α : Type u_1} (t : Ordnode α) :
                            theorem Ordnode.splitMin_eq {α : Type u_1} (s : ) (l : Ordnode α) (x : α) (r : Ordnode α) :
                            l.splitMin' x r = (l.findMin' x, (node s l x r).eraseMin)
                            theorem Ordnode.splitMax_eq {α : Type u_1} (s : ) (l : Ordnode α) (x : α) (r : Ordnode α) :
                            l.splitMax' x r = ((node s l x r).eraseMax, findMax' x r)
                            theorem Ordnode.findMin'_all {α : Type u_1} {P : αProp} (t : Ordnode α) (x : α) :
                            All P tP xP (t.findMin' x)
                            theorem Ordnode.findMax'_all {α : Type u_1} {P : αProp} (x : α) (t : Ordnode α) :
                            P xAll P tP (findMax' x t)

                            glue #

                            merge #

                            @[simp]
                            theorem Ordnode.merge_nil_left {α : Type u_1} (t : Ordnode α) :
                            t.merge nil = t
                            @[simp]
                            theorem Ordnode.merge_nil_right {α : Type u_1} (t : Ordnode α) :
                            nil.merge t = t
                            @[simp]
                            theorem Ordnode.merge_node {α : Type u_1} {ls : } {ll : Ordnode α} {lx : α} {lr : Ordnode α} {rs : } {rl : Ordnode α} {rx : α} {rr : Ordnode α} :
                            (node ls ll lx lr).merge (node rs rl rx rr) = if delta * ls < rs then ((node ls ll lx lr).merge rl).balanceL rx rr else if delta * rs < ls then ll.balanceR lx (lr.merge (node rs rl rx rr)) else (node ls ll lx lr).glue (node rs rl rx rr)

                            insert #

                            theorem Ordnode.dual_insert {α : Type u_1} [LE α] [IsTotal α fun (x1 x2 : α) => x1 x2] [DecidableLE α] (x : α) (t : Ordnode α) :

                            balance properties #

                            theorem Ordnode.balance_eq_balance' {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : l.Balanced) (hr : r.Balanced) (sl : l.Sized) (sr : r.Sized) :
                            l.balance x r = l.balance' x r
                            theorem Ordnode.balanceL_eq_balance {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (sl : l.Sized) (sr : r.Sized) (H1 : l.size = 0r.size 1) (H2 : 1 l.size1 r.sizer.size delta * l.size) :
                            l.balanceL x r = l.balance x r
                            def Ordnode.Raised (n m : ) :

                            Raised n m means m is either equal or one up from n.

                            Equations
                            Instances For
                              theorem Ordnode.raised_iff {n m : } :
                              Raised n m n m m n + 1
                              theorem Ordnode.Raised.dist_le {n m : } (H : Raised n m) :
                              n.dist m 1
                              theorem Ordnode.Raised.dist_le' {n m : } (H : Raised n m) :
                              m.dist n 1
                              theorem Ordnode.Raised.add_left (k : ) {n m : } (H : Raised n m) :
                              Raised (k + n) (k + m)
                              theorem Ordnode.Raised.add_right (k : ) {n m : } (H : Raised n m) :
                              Raised (n + k) (m + k)
                              theorem Ordnode.Raised.right {α : Type u_1} {l : Ordnode α} {x₁ x₂ : α} {r₁ r₂ : Ordnode α} (H : Raised r₁.size r₂.size) :
                              Raised (l.node' x₁ r₁).size (l.node' x₂ r₂).size
                              theorem Ordnode.balanceL_eq_balance' {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : l.Balanced) (hr : r.Balanced) (sl : l.Sized) (sr : r.Sized) (H : (∃ (l' : ), Raised l' l.size BalancedSz l' r.size) ∃ (r' : ), Raised r.size r' BalancedSz l.size r') :
                              l.balanceL x r = l.balance' x r
                              theorem Ordnode.balance_sz_dual {α : Type u_1} {l r : Ordnode α} (H : (∃ (l' : ), Raised l.size l' BalancedSz l' r.size) ∃ (r' : ), Raised r' r.size BalancedSz l.size r') :
                              (∃ (l' : ), Raised l' r.dual.size BalancedSz l' l.dual.size) ∃ (r' : ), Raised l.dual.size r' BalancedSz r.dual.size r'
                              theorem Ordnode.size_balanceL {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : l.Balanced) (hr : r.Balanced) (sl : l.Sized) (sr : r.Sized) (H : (∃ (l' : ), Raised l' l.size BalancedSz l' r.size) ∃ (r' : ), Raised r.size r' BalancedSz l.size r') :
                              (l.balanceL x r).size = l.size + r.size + 1
                              theorem Ordnode.all_balanceL {α : Type u_1} {P : αProp} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : l.Balanced) (hr : r.Balanced) (sl : l.Sized) (sr : r.Sized) (H : (∃ (l' : ), Raised l' l.size BalancedSz l' r.size) ∃ (r' : ), Raised r.size r' BalancedSz l.size r') :
                              All P (l.balanceL x r) All P l P x All P r
                              theorem Ordnode.balanceR_eq_balance' {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : l.Balanced) (hr : r.Balanced) (sl : l.Sized) (sr : r.Sized) (H : (∃ (l' : ), Raised l.size l' BalancedSz l' r.size) ∃ (r' : ), Raised r' r.size BalancedSz l.size r') :
                              l.balanceR x r = l.balance' x r
                              theorem Ordnode.size_balanceR {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : l.Balanced) (hr : r.Balanced) (sl : l.Sized) (sr : r.Sized) (H : (∃ (l' : ), Raised l.size l' BalancedSz l' r.size) ∃ (r' : ), Raised r' r.size BalancedSz l.size r') :
                              (l.balanceR x r).size = l.size + r.size + 1
                              theorem Ordnode.all_balanceR {α : Type u_1} {P : αProp} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : l.Balanced) (hr : r.Balanced) (sl : l.Sized) (sr : r.Sized) (H : (∃ (l' : ), Raised l.size l' BalancedSz l' r.size) ∃ (r' : ), Raised r' r.size BalancedSz l.size r') :
                              All P (l.balanceR x r) All P l P x All P r
                              def Ordnode.Bounded {α : Type u_1} [Preorder α] :
                              Ordnode αWithBot αWithTop αProp

                              Bounded t lo hi says that every element x ∈ t is in the range lo < x < hi, and also this property holds recursively in subtrees, making the full tree a BST. The bounds can be set to lo = ⊥ and hi = ⊤ if we care only about the internal ordering constraints.

                              Equations
                              Instances For
                                theorem Ordnode.Bounded.dual {α : Type u_1} [Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} :
                                t.Bounded o₁ o₂t.dual.Bounded o₂ o₁
                                theorem Ordnode.Bounded.dual_iff {α : Type u_1} [Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} :
                                t.Bounded o₁ o₂ t.dual.Bounded o₂ o₁
                                theorem Ordnode.Bounded.weak_left {α : Type u_1} [Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} :
                                t.Bounded o₁ o₂t.Bounded o₂
                                theorem Ordnode.Bounded.weak_right {α : Type u_1} [Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} :
                                t.Bounded o₁ o₂t.Bounded o₁
                                theorem Ordnode.Bounded.weak {α : Type u_1} [Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (h : t.Bounded o₁ o₂) :
                                theorem Ordnode.Bounded.mono_left {α : Type u_1} [Preorder α] {x y : α} (xy : x y) {t : Ordnode α} {o : WithTop α} :
                                t.Bounded (↑y) ot.Bounded (↑x) o
                                theorem Ordnode.Bounded.mono_right {α : Type u_1} [Preorder α] {x y : α} (xy : x y) {t : Ordnode α} {o : WithBot α} :
                                t.Bounded o xt.Bounded o y
                                theorem Ordnode.Bounded.to_lt {α : Type u_1} [Preorder α] {t : Ordnode α} {x y : α} :
                                t.Bounded x yx < y
                                theorem Ordnode.Bounded.to_nil {α : Type u_1} [Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} :
                                t.Bounded o₁ o₂nil.Bounded o₁ o₂
                                theorem Ordnode.Bounded.trans_left {α : Type u_1} [Preorder α] {t₁ t₂ : Ordnode α} {x : α} {o₁ : WithBot α} {o₂ : WithTop α} :
                                t₁.Bounded o₁ xt₂.Bounded (↑x) o₂t₂.Bounded o₁ o₂
                                theorem Ordnode.Bounded.trans_right {α : Type u_1} [Preorder α] {t₁ t₂ : Ordnode α} {x : α} {o₁ : WithBot α} {o₂ : WithTop α} :
                                t₁.Bounded o₁ xt₂.Bounded (↑x) o₂t₁.Bounded o₁ o₂
                                theorem Ordnode.Bounded.mem_lt {α : Type u_1} [Preorder α] {t : Ordnode α} {o : WithBot α} {x : α} :
                                t.Bounded o xAll (fun (x_1 : α) => x_1 < x) t
                                theorem Ordnode.Bounded.mem_gt {α : Type u_1} [Preorder α] {t : Ordnode α} {o : WithTop α} {x : α} :
                                t.Bounded (↑x) oAll (fun (x_1 : α) => x_1 > x) t
                                theorem Ordnode.Bounded.of_lt {α : Type u_1} [Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} {x : α} :
                                t.Bounded o₁ o₂nil.Bounded o₁ xAll (fun (x_1 : α) => x_1 < x) tt.Bounded o₁ x
                                theorem Ordnode.Bounded.of_gt {α : Type u_1} [Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} {x : α} :
                                t.Bounded o₁ o₂nil.Bounded (↑x) o₂All (fun (x_1 : α) => x_1 > x) tt.Bounded (↑x) o₂
                                theorem Ordnode.Bounded.to_sep {α : Type u_1} [Preorder α] {t₁ t₂ : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} {x : α} (h₁ : t₁.Bounded o₁ x) (h₂ : t₂.Bounded (↑x) o₂) :
                                All (fun (y : α) => All (fun (z : α) => y < z) t₂) t₁