instWellFoundedLTAntisymmetrizationLe

English

If α has a well-founded LT, then Antisymmetrization α with respect to ≤ also has a well-founded LT.

Русский

Если у α есть хорошо основанное LT, то антисимметризация α по ≤ также имеет хорошо основанное LT.

LaTeX

$$$[\\text{WellFoundedLT } α] \\Rightarrow [\\text{WellFoundedLT } (\\text{Antisymmetrization}(α, ≤))]$$$

Lean4

instance [WellFoundedLT α] : WellFoundedLT (Antisymmetrization α (· ≤ ·)) :=
  wellFoundedLT_antisymmetrization_iff.mpr ‹_›

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