wellFoundedGT — Mathlib

English

If α and β have descending chains in the GT order, then α × β has descending chains in the GT order, transported through antisymmetrization.

Русский

Если у α и β есть нисходящие последовательности в порядке GT, то и у их произведения α × β существуют нисходящие последовательности в GT через антисимметризацию.

LaTeX

$$$\\text{WellFoundedGT}(α) \\land \\text{WellFoundedGT}(β) \\Rightarrow \\text{WellFoundedGT}(α × β)$$$

Lean4

instance wellFoundedGT [WellFoundedGT α] [WellFoundedGT β] : WellFoundedGT (α × β) :=
  wellFoundedGT_antisymmetrization_iff.mp <| (Antisymmetrization.prodEquiv α β).strictMono.wellFoundedGT

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