English
Under suitable order-theoretic hypotheses on α and β (PartialOrder with WellFoundedLT, and Preorder with WellFoundedLT), the product α × β with Prod.Lex (<) (<) is WellFoundedLT.
Русский
При соответствующих условиях порядка на $\alpha$ и $\beta$ (PartialOrder и WellFoundedLT), произведение $\alpha\times\beta$ с лексикографическим порядком имеет WellFoundedLT.
LaTeX
$$WellFoundedLT(α × β)$$
Lean4
/-- See `Prod.wellFoundedLT` for a version that only requires `Preorder α`. -/
theorem wellFoundedLT' [PartialOrder α] [WellFoundedLT α] [Preorder β] [WellFoundedLT β] : WellFoundedLT (α × β) :=
Subrelation.isWellFounded (Prod.Lex (· < ·) (· < ·)) fun {x y} h ↦
(Prod.lt_iff.mp h).elim (fun h ↦ .left _ _ h.1) fun h ↦
h.1.lt_or_eq.elim (.left _ _) <| by cases x; cases y; rintro rfl; exact .right _ h.2
