wellFoundedGT' — Mathlib

English

If α and β satisfy the dual conditions to LT' (PartialOrder and WellFoundedGT), then the product α × β with Prod.Lex is WellFoundedGT.

Русский

Если $\alpha$ и $\beta$ удовлетворяют двойственным условиям LT' (PartialOrder и WellFoundedGT), то произведение $\alpha\times\beta$ с лексикографическим порядком является WellFoundedGT.

LaTeX

$$WellFoundedGT(α × β)$$

Lean4

/-- See `Prod.wellFoundedGT` for a version that only requires `Preorder α`. -/
theorem wellFoundedGT' [PartialOrder α] [WellFoundedGT α] [Preorder β] [WellFoundedGT β] : WellFoundedGT (α × β) :=
  @Prod.wellFoundedLT' αᵒᵈ βᵒᵈ _ _ _ _

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