wellFoundedLT — Mathlib

English

If α and β are well-founded in the order sense, then their product α × β is well-founded in the product order, via the antisymmetrization equivalence.

Русский

Если α и β хорошо основаны в порядке, то их произведение α × β также хорошо основано в произведении порядка, через эквивалентность антисимметризации.

LaTeX

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

Lean4

instance wellFoundedLT [WellFoundedLT α] [WellFoundedLT β] : WellFoundedLT (α × β) :=
  wellFoundedLT_antisymmetrization_iff.mp <| (Antisymmetrization.prodEquiv α β).strictMono.wellFoundedLT

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