wellFoundedGT_antisymmetrization_iff

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⟩

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