equiv_iff — Mathlib

English

Let t1 and t2 be sized Ordnodes. Then t1 is equivalent to t2 if and only if their toList representations are equal.

Русский

Пусть t1 и t2 — упорядоченные узлы размерности. Тогда t1 эквивалентен t2 тогда, когда их представления toList совпадают.

LaTeX

$$$t_1\text{ sized},\ t_2\text{ sized} \Rightarrow (\operatorname{Equiv}(t_1,t_2) \iff \operatorname{toList}(t_1) = \operatorname{toList}(t_2))$$$

Lean4

theorem equiv_iff {t₁ t₂ : Ordnode α} (h₁ : Sized t₁) (h₂ : Sized t₂) : Equiv t₁ t₂ ↔ toList t₁ = toList t₂ :=
  and_iff_right_of_imp fun h => by rw [← length_toList h₁, h, length_toList h₂]

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