English
The Lex product of indexed linear orders yields a linear order when the index type is linear and the coordinates are linear orders themselves with appropriate well-foundedness conditions.
Русский
Произведение Lex линейных порядков по индексам образует линейный порядок при условии линейности индекса и порядка координат вместе с необходимыми условиями.
LaTeX
$$$\\text{Lex}((i\\mapsto \\beta_i))$ is a linear order given the assumptions$$
Lean4
/-- `Lex (∀ i, α i)` is a linear order if the original order has well-founded `<`. -/
noncomputable instance linearOrder [LinearOrder ι] [WellFoundedLT ι] [∀ a, LinearOrder (β a)] :
LinearOrder (Lex (∀ i, β i)) :=
@linearOrderOfSTO (Πₗ i, β i) (· < ·) { trichotomous := (isTrichotomous_lex _ _ IsWellFounded.wf).1 }
(Classical.decRel _)
