dual — Mathlib

English

The boundedness property is preserved under the dual (order-reversed) tree, in the sense that Bounded t o1 o2 is equivalent to Bounded t^dual o2 o1 in the dual order.

Русский

Свойство ограниченности сохраняется при переходе к двойственному дереву (обратному порядку): Bounded t o1 o2 эквивалентно Bounded t^dual o2 o1 во взаимнооборотном порядке.

LaTeX

$$$\forall t\ o_1\ o_2: Bounded\ t\ o_1\ o_2 \Rightarrow Bounded(dual\ t)\ o_2\ o_1$$$

Lean4

theorem dual : ∀ {t : Ordnode α} {o₁ o₂}, Bounded t o₁ o₂ → @Bounded αᵒᵈ _ (dual t) o₂ o₁
  | nil, o₁, o₂, h => by cases o₁ <;> cases o₂ <;> trivial
  | node _ _ _ _, _, _, ⟨ol, Or⟩ => ⟨Or.dual, ol.dual⟩

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