findMax'_dual — Mathlib

English

For every Ordnode t over α, the maximum of its dual equals the minimum of t: 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) (x : α) : findMax' x (dual t) = findMin' t x := by rw [← findMin'_dual, dual_dual]

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