dual_eraseMin — Mathlib

English

Erasing the minimum in a tree corresponds to erasing the maximum in the dual tree: dual (eraseMin t) = eraseMax (dual t).

Русский

Удаление минимального элемента в дереве соответствует удалению максимального в двойственном дереве: dual (eraseMin t) = eraseMax (dual t).

LaTeX

$$$\operatorname{dual}(\operatorname{eraseMin}(t)) = \operatorname{eraseMax}(\operatorname{dual}(t))$$$

Lean4

theorem dual_eraseMin : ∀ t : Ordnode α, dual (eraseMin t) = eraseMax (dual t)
  | nil => rfl
  | node _ nil _ _ => rfl
  | node _ (node sz l' y r') x r => by
    rw [eraseMin, dual_balanceR, dual_eraseMin (node sz l' y r'), dual, dual, dual, eraseMax]

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