splitMin_eq — Mathlib

English

For any s, l, x, r, the operation splitMin' l x r yields the pair (findMin' l x, eraseMin (node s l x r)).

Русский

Для любых s, l, x, r операция splitMin' l x r возвращает пары (findMin'(l,x), eraseMin(узел s l x r)).

LaTeX

$$\forall s l x r,\; splitMin'(l,x,r) = (findMin'(l,x), eraseMin(\operatorname{node} s l x r))$$

Lean4

theorem splitMin_eq : ∀ (s l) (x : α) (r), splitMin' l x r = (findMin' l x, eraseMin (node s l x r))
  | _, nil, _, _ => rfl
  | _, node ls ll lx lr, x, r => by rw [splitMin', splitMin_eq ls ll lx lr, findMin', eraseMin]

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