wellFoundedLT_antisymmetrization_iff

English

Equivalence between well-foundedness of LT on Antisymmetrization and LT on α, via lifting two-variable well-foundedness equivalence.

Русский

Эквивалентность обоснованности LT на антисимметризации и LT на α через двойную подъемную эквивалентность.

LaTeX

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

Lean4

theorem wellFoundedLT_antisymmetrization_iff : WellFoundedLT (Antisymmetrization α (· ≤ ·)) ↔ WellFoundedLT α := by
  simp_rw [isWellFounded_iff, wellFounded_antisymmetrization_iff]

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