split3 — Mathlib

English

If left and right parts are valid and a balancing hypothesis holds, then balanceL preserves validity between the outer contexts after reassembling the tree.

Русский

Если левая и правая части корректны и выполняется условие балансировки, то balanceL сохраняет корректность при сборке дерева во внешнем контексте.

LaTeX

$$$\\text{balanceL}:\\ text{Valid'} o_1 l x r \\to \\text{Valid'} x r o_2 \\to \\text{(H)} \\Rightarrow \\text{Valid'} o_1 (l\\!\\balanceL\\ x\\ r) o_2$$$

Lean4

/-- O(log n). Split the tree into those smaller than `x` and those greater than it,
plus an element equivalent to `x`, if it exists.

    split3 2 {1, 2, 4} = ({1}, some 2, {4})
    split3 3 {1, 2, 4} = ({1, 2}, none, {4})
    split3 4 {1, 2, 4} = ({1, 2}, some 4, ∅)

Using a preorder on `ℕ × ℕ` that only compares the first coordinate:

    split3 (1, 1) {(0, 1), (1, 2)} = ({(0, 1)}, some (1, 2), ∅)
    split3 (3, 1) {(0, 1), (1, 2)} = ({(0, 1), (1, 2)}, none, ∅) -/
def split3 (x : α) : Ordnode α → Ordnode α × Option α × Ordnode α
  | nil => (nil, none, nil)
  | node _ l y r =>
    match cmpLE x y with
    | Ordering.lt =>
      let (lt, f, gt) := split3 x l
      (lt, f, link gt y r)
    | Ordering.eq => (l, some y, r)
    | Ordering.gt =>
      let (lt, f, gt) := split3 x r
      (link l y lt, f, gt)

Похожие утверждения