acc_antisymmetrization_iff — Mathlib

English

Acc (less-than) on the antisymmetrized structure is equivalent to Acc on the original preorder.

Русский

Acc выражения относительно антисимметризации равносильно Acc для исходного предпорядка.

LaTeX

$$$\\text{Acc}(<)\\big(\\text{toAntisymmetrization}(α, ≤)\\, a\\right) \\iff \\text{Acc}(<, a)$$$

Lean4

theorem acc_antisymmetrization_iff : Acc (· < ·) (toAntisymmetrization (α := α) (· ≤ ·) a) ↔ Acc (· < ·) a :=
  acc_lift₂_iff

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