dual_iff — Mathlib

English

Validity of t in the original order is equivalent to validity of its dual in the reversed order.

Русский

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

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 α} : Valid t ↔ @Valid αᵒᵈ _ (.dual t) :=
  Valid'.dual_iff

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