instWellFoundedGTAntisymmetrizationLe

English

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

Русский

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

LaTeX

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

Lean4

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

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