findMax_dual — Mathlib

English

For any Ordnode t, the maximum in the dual tree is the minimum in the original: findMax(dual t) = findMin t.

Русский

Для любого дерева Ordnode максимум в двойственном дереве равен минимуму в исходном: findMax(dual t) = findMin t.

LaTeX

$$$\operatorname{findMax}(\operatorname{dual}(t)) = \operatorname{findMin}(t)$$$

Lean4

theorem findMax_dual (t : Ordnode α) : findMax (dual t) = findMin t := by rw [← findMin_dual, dual_dual]

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