splitMax_eq — Mathlib

English

For any s, l, x, r, splitMax' l x r equals (eraseMax (node s l x r), findMax' x r).

Русский

Для любых s, l, x, r splitMax' l x r равно (eraseMax (node s l x r), findMax' x r).

LaTeX

$$\forall s l x r,\; splitMax'(l,x,r) = (eraseMax(\operatorname{node} s l x r), findMax'(x,r))$$

Lean4

theorem splitMax_eq : ∀ (s l) (x : α) (r), splitMax' l x r = (eraseMax (node s l x r), findMax' x r)
  | _, _, _, nil => rfl
  | _, l, x, node ls ll lx lr => by rw [splitMax', splitMax_eq ls ll lx lr, findMax', eraseMax]

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