dual_eraseMax — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem dual_eraseMax (t : Ordnode α) : dual (eraseMax t) = eraseMin (dual t) := by
  rw [← dual_dual (eraseMin _), dual_eraseMin, dual_dual]

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