English
Well-foundedness of the GT relation on Antisymmetrization is equivalent to well-foundedness of GT on α.
Русский
Обоснованность отношения GT на антисимметризации эквивалентна обоснованности GT на α.
LaTeX
$$$\\text{WellFoundedGT}(\\text{Antisymmetrization}(α, ≤)) \\iff \\text{WellFoundedGT}(α)$$$
Lean4
theorem wellFoundedGT_antisymmetrization_iff : WellFoundedGT (Antisymmetrization α (· ≤ ·)) ↔ WellFoundedGT α :=
by
simp_rw [isWellFounded_iff]
convert wellFounded_liftOn₂'_iff with ⟨_⟩ ⟨_⟩
exact fun _ _ _ _ h₁ h₂ ↦ propext ⟨fun h ↦ (h₂.2.trans_lt h).trans_le h₁.1, fun h ↦ (h₂.1.trans_lt h).trans_le h₁.2⟩