wellFounded_antisymmetrization_iff

English

Well-foundedness of LT on the antisymmetrization is equivalent to well-foundedness of LT on α.

Русский

Сопряжённость WellFounded LT на антисимметризации эквивалентна WellFounded LT на α.

LaTeX

$$$\\text{WellFoundedLT}(\\text{Antisymmetrization}(α, ≤)) \\iff \\text{WellFoundedLT}(α)$$$

Lean4

theorem wellFounded_antisymmetrization_iff :
    WellFounded (@LT.lt (Antisymmetrization α (· ≤ ·)) _) ↔ WellFounded (@LT.lt α _) :=
  wellFounded_lift₂_iff

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