dual_iff — Mathlib

English

The boundedness of a tree is equivalent to the boundedness of its dual with swapped bounds.

Русский

Ограниченность дерева эквивалентна ограниченности его двойника при обмене границ.

LaTeX

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

Lean4

theorem dual_iff {t : Ordnode α} {o₁ o₂} : Bounded t o₁ o₂ ↔ @Bounded αᵒᵈ _ (.dual t) o₂ o₁ :=
  ⟨Bounded.dual, fun h => by have := Bounded.dual h; rwa [dual_dual, OrderDual.Preorder.dual_dual] at this⟩

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