English
Dickson-type lemma for finite-index families: if each α i has a linear order and is well-ordered, then the set of all functions i ↦ α i is PWOn; in particular, ℕ^n is PWOn.
Русский
Лемма Диксона для семей с конечным индексом: если каждый α_i является линейным порядком и хорошо упорядочен, тогда множество функций i ↦ α_i является PWOn; в частности ℕ^n — PWOn.
LaTeX
$$isPWO {α : ι → Type*} [∀ i, LinearOrder (α i)] [∀ i, IsWellOrder (α i) (· < ·)] [Finite ι] (s : Set (∀ i, α i)) : s.IsPWO$$
Lean4
theorem ProdLex_iff [PartialOrder α] [Preorder β] {s : Set (α ×ₗ β)} :
s.IsPWO ↔ ((fun (x : α ×ₗ β) ↦ (ofLex x).1) '' s).IsPWO ∧ ∀ a, {y | toLex (a, y) ∈ s}.IsPWO :=
⟨fun h ↦ ⟨imageProdLex h, fiberProdLex h⟩, fun h ↦ subsetProdLex h.1 h.2⟩
