English
If each coordinate carries a Preorder and ι is well-founded and linear, then Lex forms a strict order on the product.
Русский
Если каждое измерение даёт предикат упорядочивания и множество индексов упорядовано линейно и хорошо упорядочено, то Lex образует строгий порядок на произведение.
LaTeX
$$$\\text{Lex}((i\\mapsto \\beta_i))\\;\\text{is a linear/strict order under appropriate conditions}$$$
Lean4
theorem lex_lt_of_lt_of_preorder [∀ i, Preorder (β i)] {r} (hwf : WellFounded r) {x y : ∀ i, β i} (hlt : x < y) :
∃ i, (∀ j, r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i :=
let h' := Pi.lt_def.1 hlt
let ⟨i, hi, hl⟩ := hwf.has_min _ h'.2
⟨i, fun j hj => ⟨h'.1 j, not_not.1 fun h => hl j (lt_of_le_not_ge (h'.1 j) h) hj⟩, hi⟩
