instWellQuasiOrderedLEProd — Mathlib

English

The product of two WellQuasiOrderedLE structures is WellQuasiOrderedLE on the product.

Русский

Произведение двух структур WellQuasiOrderedLE образует WellQuasiOrderedLE на произведении.

LaTeX

$$$[\\text{WellQuasiOrderedLE }\\alpha] [\\text{WellQuasiOrderedLE }\\beta] \\Rightarrow \\mathrm{WellQuasiOrderedLE}(\\mathrm{Prod}\\ \\alpha\\ \\beta)$$$

Lean4

instance [WellQuasiOrderedLE α] [Preorder β] [WellQuasiOrderedLE β] : WellQuasiOrderedLE (α × β) :=
  ⟨wellQuasiOrdered_le.prod wellQuasiOrdered_le⟩

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