Ordnode.dual_dual
theorem Ordnode.dual_dual : ∀ {α : Type u_1} (t : Ordnode α), t.dual.dual = t
This theorem, `Ordnode.dual_dual`, states that for any type `α` and any value `t` of type `Ordnode α`, applying the `Ordnode.dual` function twice to `t` returns `t` itself. In other words, the `Ordnode.dual` function is its own inverse when applied twice.
More concisely: For any type `α` and any `Ordnode α` value `t`, applying the `Ordnode.dual` function twice to `t` results in `t`. That is, `Ordnode.dual (Ordnode.dual t) = t`.
|
Mathlib.Data.Ordmap.Ordset._auxLemma.6
theorem Mathlib.Data.Ordmap.Ordset._auxLemma.6 :
∀ {α : Type u_1} {P : α → Prop} {l : Ordnode α} {x : α} {r : Ordnode α},
Ordnode.All P (l.node' x r) = (Ordnode.All P l ∧ P x ∧ Ordnode.All P r)
The theorem `Mathlib.Data.Ordmap.Ordset._auxLemma.6` states that for any type `α`, property `P` that each element of type `α` can have, and ordered nodes `l`, `x`, and `r`, the predicate `Ordnode.All P` applied to the node created by `Ordnode.node' l x r` (without rebalancing) is equivalent to the conjunction (logical "and") of `Ordnode.All P l`, `P x`, and `Ordnode.All P r`. In other words, every element in the balanced tree (comprising of nodes `l`, `x`, and `r`) satisfies `P` if and only if every element in `l`, `x`, and `r` individually satisfies `P`.
More concisely: For any type `α` and property `P`, the node `Ordnode.node' l x r` in an ordered tree satisfies `Ordnode.All P` if and only if nodes `l`, `x`, and `r` individually satisfy `P`.
|
Ordnode.dual_rotateR
theorem Ordnode.dual_rotateR :
∀ {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α), (l.rotateR x r).dual = r.dual.rotateL x l.dual
The theorem `Ordnode.dual_rotateR` states that for any type `α`, and for any ordered nodes `l` and `r`, and an element `x` of the type `α`, the operation of taking the dual of the right rotation of `l`, `x`, and `r` is equal to the left rotation of the dual of `r`, `x`, and the dual of `l`. Here, duality refers to the operation of reversing the order of elements in the ordered node structure, while right and left rotations are operations used to balance binary search trees after insertions or deletions.
More concisely: For any type `α` and ordered nodes `l`, `r`, and `x` of type `α`, the dual of the right rotation of `l`, `x`, and `r` equals the left rotation of the dual of `r`, `x`, and the dual of `l`.
|
Ordnode.dual_balanceR
theorem Ordnode.dual_balanceR :
∀ {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α), (l.balanceR x r).dual = r.dual.balanceL x l.dual := by
sorry
The theorem `Ordnode.dual_balanceR` states that for all types `α`, and for all ordered nodes `l` and `r` of type `α`, the function `dual` applied to the right-balanced tree formed with `l`, `x`, and `r` (i.e., `Ordnode.balanceR l x r`) will be equivalent to the left-balanced tree formed with the dual of `r`, `x`, and the dual of `l` (i.e., `Ordnode.balanceL (Ordnode.dual r) x (Ordnode.dual l)`). This shows a symmetry in the dual operations of right balancing and left balancing in an ordered binary tree.
More concisely: For all types `α` and ordered nodes `l`, `x`, and `r` of type `α`, `Ordnode.balanceR l x r` is dual to `Ordnode.balanceL (Ordnode.dual r) x (Ordnode.dual l)`.
|
Ordnode.Valid'.node'
theorem Ordnode.Valid'.node' :
∀ {α : Type u_1} [inst : Preorder α] {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
Ordnode.Valid' o₁ l ↑x →
Ordnode.Valid' (↑x) r o₂ → Ordnode.BalancedSz l.size r.size → Ordnode.Valid' o₁ (l.node' x r) o₂
This theorem, `Ordnode.Valid'.node'`, asserts that for any type `α` which has a preorder relation, given a left Ordnode `l`, a value `x` of type `α`, a right Ordnode `r`, and two optional types `o₁` and `o₂` (which can be thought of as possible maximum and minimum bounds), if `l` is a valid Ordnode with respect to `o₁` and `x`, and `r` is a valid Ordnode with respect to `x` and `o₂`, and if the sizes of `l` and `r` satisfy the `Ordnode.BalancedSz` condition (meaning that either their sum is less than or equal to 1, or each one is less than or equal to `Ordnode.delta` times the other), then the new Ordnode created by `Ordnode.node'` with `l`, `x`, and `r` is also a valid Ordnode with respect to `o₁` and `o₂`. This essentially states that constructing a new Ordnode with correct size information from valid child nodes gives you a valid parent node, assuming that the sizes of the child nodes satisfy the balance condition.
More concisely: If `α` has a preorder relation, `l` is a valid Ordnode with respect to optional `o₁` and `x`, `r` is a valid Ordnode with respect to `x` and `o₂`, and their sizes satisfy the `Ordnode.BalancedSz` condition, then the new Ordnode created by `Ordnode.node'` with `l`, `x`, and `r` is also a valid Ordnode with respect to `o₁` and `o₂`.
|
Ordnode.Bounded.to_lt
theorem Ordnode.Bounded.to_lt :
∀ {α : Type u_1} [inst : Preorder α] {t : Ordnode α} {x y : α}, t.Bounded ↑x ↑y → x < y
This theorem states that for any type `α` with a preorder, and for any Ordnode `t` of type `α`, along with any two elements `x` and `y` of type `α`, if the Ordnode `t` is bounded by `x` and `y`, then `x` is strictly less than `y`. It's essentially a property of the 'bounded' condition in the context of ordered nodes or Ordnode. This theorem is proven under the assumption that the provided type `α` has a preorder, which is a binary relation that is reflexive and transitive.
More concisely: If `α` is a type with a preorder, and `t` is an Ordnode of `α` bounded by elements `x` and `y` of `α`, then `x` strictly precedes `y` in the preorder.
|
Ordnode.BalancedSz.symm
theorem Ordnode.BalancedSz.symm : ∀ {l r : ℕ}, Ordnode.BalancedSz l r → Ordnode.BalancedSz r l
The theorem `Ordnode.BalancedSz.symm` states that for any two natural numbers `l` and `r`, if the hypothetical tree with children of sizes `l` and `r` is balanced according to the `Ordnode.BalancedSz` definition, then the hypothetical tree with children of sizes `r` and `l` is also balanced. In other words, the balance condition is symmetric with respect to swapping the sizes of the left and right subtrees.
More concisely: If a binary tree is balanced according to `Ordnode.BalancedSz` definition with left child of size `l` and right child of size `r`, then it is also balanced with left child of size `r` and right child of size `l`.
|
Ordnode.Sized.node'
theorem Ordnode.Sized.node' :
∀ {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α}, l.Sized → r.Sized → (l.node' x r).Sized
The theorem `Ordnode.Sized.node'` states that for any type `α`, for any left and right nodes (`l` and `r` respectively) of type `Ordnode α`, and for any node `x` of type `α`, if the left node `l` and the right node `r` all have the `Sized` property (i.e., the `size` field in the node matches the actual size of the subtree), then the node created by `Ordnode.node'` function applied to `l`, `x`, and `r` also has the `Sized` property. In other words, constructing a new node with the correct size information, without rebalancing, preserves the `Sized` property.
More concisely: For any type `α` and `Ordnode α` nodes `l`, `r`, and `x` with the `Sized` property, the node created by `Ordnode.node'` function also has the `Sized` property.
|
Mathlib.Data.Ordmap.Ordset._auxLemma.7
theorem Mathlib.Data.Ordmap.Ordset._auxLemma.7 : ∀ {a b c : Prop}, ((a ∧ b) ∧ c) = (a ∧ b ∧ c)
This theorem, `Mathlib.Data.Ordmap.Ordset._auxLemma.7`, asserts that for any three propositions `a`, `b`, and `c`, the proposition "`a` and `b` are both true, and also `c` is true" is logically equivalent to the proposition "`a` is true, and both `b` and `c` are true". In other words, the logical conjunction operator (`∧`) is associative, so the grouping of `a`, `b`, and `c` in `(a ∧ b) ∧ c` and `a ∧ (b ∧ c)` does not matter.
More concisely: The theorem `Mathlib.Data.Ordmap.Ordset._auxLemma.7` in Lean 4 states that the logical conjunction `(a ∧ b) ∧ c` is logically equivalent to `a ∧ (b ∧ c)` for any propositions `a`, `b`, and `c`. In other words, the logical conjunction operator is associative in Lean.
|
Ordnode.Valid'.dual
theorem Ordnode.Valid'.dual :
∀ {α : Type u_1} [inst : Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
Ordnode.Valid' o₁ t o₂ → Ordnode.Valid' o₂ t.dual o₁
This theorem is about the validity of a dual operation on an ordered node in the context of ordered trees. Specifically, for any type `α` equipped with a preorder, given an ordered node `t` of type `α`, and two other elements `o₁` of type `α` attached with bottom (`⊥`) and `o₂` of type `α` attached with top (`⊤`), if the ordered node `t` is valid between `o₁` and `o₂` (i.e., `Ordnode.Valid' o₁ t o₂` is true), then the dual of the ordered node `t` is valid between `o₂` and `o₁` (i.e., `Ordnode.Valid' o₂ (Ordnode.dual t) o₁` is also true). This theorem essentially establishes the validity of a reversal operation in the context of ordered trees.
More concisely: For any ordered node `t` in an ordered tree with respect to a preorder, if `Ordnode.Valid' o₁ t o₂` holds, then `Ordnode.Valid' o₂ (Ordnode.dual t) o₁` also holds. (The dual of an ordered node `t` reverses the order relationship between its elements.)
|
Ordnode.balanceL_eq_balance'
theorem Ordnode.balanceL_eq_balance' :
∀ {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α},
l.Balanced →
r.Balanced →
l.Sized →
r.Sized →
((∃ l', Ordnode.Raised l' l.size ∧ Ordnode.BalancedSz l' r.size) ∨
∃ r', Ordnode.Raised r.size r' ∧ Ordnode.BalancedSz l.size r') →
l.balanceL x r = l.balance' x r
The theorem `Ordnode.balanceL_eq_balance'` states that for any type `α`, and for any ordinal nodes `l` and `r` and an instance `x` of type `α`, if both `l` and `r` are balanced and their respective sizes as stated match their actual sizes, and there exists a size `l'` that is equal to or one-up from the size of `l` and a hypothetical tree with children of sizes `l'` and size of `r` is balanced, or there exists a size `r'` that is equal to or one-up from the size of `r` and a hypothetical tree with children of sizes size of `l` and `r'` is balanced, then the balance of `l`, `x`, and `r` is equivalent to the full balance operation on `l`, `x` and `r`. In other words, the simple balance operation is equivalent to the full balance operation under the given conditions.
More concisely: Given ordinal nodes `l`, `r` of type `α` with matched sizes, and instances `x` of `α`, if both `l` and `r` are balanced and the hypothetical trees with children sizes `l' = size l + 1` and `r` or `l` and `r' = size r + 1` are balanced, then `balance l x r` equals the full balance operation on `l`, `x`, and `r`.
|
Ordnode.size_dual
theorem Ordnode.size_dual : ∀ {α : Type u_1} (t : Ordnode α), t.dual.size = t.size
This theorem, `Ordnode.size_dual`, states that for any type `α` and any instance `t` of an `Ordnode` of type `α`, the size of the `Ordnode` when passed through the `dual` function is equal to the original size of the `Ordnode`. In other words, the dual operation does not change the size of an `Ordnode`.
More concisely: For any type `α` and `Ordnode` instance `t` of type `Ordnode α`, the size of `dual (Ordnode.mk node x)` equals the size of `Ordnode.mk node x`, where `node` is any node and `x` is any element of type `α`.
|
Ordnode.Valid'.valid
theorem Ordnode.Valid'.valid :
∀ {α : Type u_1} [inst : Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
Ordnode.Valid' o₁ t o₂ → t.Valid
This theorem states that for any type `α` under a preorder, for any `Ordnode` of type `α`, and for any `WithBot α` and `WithTop α`, if the `Ordnode` is valid in the sense of the `Ordnode.Valid'` predicate with respect to these boundary conditions, then the `Ordnode` is also valid in the sense of the `Ordnode.Valid` predicate. In other words, it ensures that the properties tested by `Ordnode.Valid'`, which includes the correctness of the `size` fields, the balance of the tree, and the organization of elements according to the ordering, are also implied by the `Ordnode.Valid` predicate.
More concisely: For any type `α` under a preorder, if an `Ordnode` of type `α` is valid with respect to given boundary conditions `WithBot` and `WithTop` in the sense of `Ordnode.Valid'`, then it is also valid in the sense of `Ordnode.Valid`.
|
Ordnode.Sized.dual
theorem Ordnode.Sized.dual : ∀ {α : Type u_1} {t : Ordnode α}, t.Sized → t.dual.Sized
The theorem `Ordnode.Sized.dual` states that for any type `α` and any ordered node `t` of that type, if the ordered node `t` satisfies the `Sized` property (meaning that all the `size` fields in its nodes match the actual size of the respective subtrees), then the dual of the ordered node `t` also satisfies the `Sized` property. In other words, the `Sized` property is preserved when taking the dual of an ordered node.
More concisely: If `α` is a type and `t` is an ordered node of type `α` with the `Sized` property, then the dual of `t` also has the `Sized` property.
|
Ordnode.Valid'.dual_iff
theorem Ordnode.Valid'.dual_iff :
∀ {α : Type u_1} [inst : Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
Ordnode.Valid' o₁ t o₂ ↔ Ordnode.Valid' o₂ t.dual o₁
The theorem `Ordnode.Valid'.dual_iff` states that for any given type `α` which is a Preorder, any Ordnode `t` of `α`, any element `o₁` of `WithBot α`, and any element `o₂` of `WithTop α`, the Ordnode `t` is valid with respect to `o₁` and `o₂` if and only if the dual of `Ordnode t` is valid with respect to `o₂` and `o₁`. Here, `WithBot α` and `WithTop α` essentially extend `α` by attaching a bottom element `⊥` and a top element `⊤` respectively, `Ordnode` is a type of self-balancing binary search trees, and `Ordnode.Valid'` is a predicate that checks if the tree is valid with respect to two optional bounds. The 'dual' of a tree is obtained by flipping it around the root, which turns a tree valid for `o₁` and `o₂` into one valid for `o₂` and `o₁`.
More concisely: For any Preorder type `α`, Ordnode `t` of `α`, and elements `o₁` of `WithBot α` and `o₂` of `WithTop α`, the Ordnode `t` is valid with respect to `o₁` and `o₂` if and only if the dual of Ordnode `t` is valid with respect to `o₂` and `o₁`.
|