dual_iff — Mathlib

English

Validity of a tree in a preorder is equivalent to the validity of its dual in the opposite order.

Русский

Допустимость дерева в порядке предварения эквивалентна допустимости его двойственности в противоположном порядке.

LaTeX

$$$\\forall t:\\ Ordnode(\\alpha),\\; \\operatorname{Valid}'(o_1,t,o_2) \\iff \\operatorname{Valid}'(o_2, t.dual, o_1).$$$

Lean4

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

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