English
For a linear order ι and partial orders on each coordinate, the Colex construction yields a strict order.
Русский
Для линейного порядка ι и частичных порядков по координатам конструкция Colex образует строгий порядок.
LaTeX
$$$IsStrictOrder(\\text{Colex}((i\\mapsto \\beta_i)), <)$ under the assumed structures$$
Lean4
instance isStrictOrder [LinearOrder ι] [∀ a, PartialOrder (β a)] : IsStrictOrder (Lex (∀ i, β i)) (· < ·)
where
irrefl := fun a ⟨k, _, hk₂⟩ => lt_irrefl (a k) hk₂
trans := by
rintro a b c ⟨N₁, lt_N₁, a_lt_b⟩ ⟨N₂, lt_N₂, b_lt_c⟩
rcases lt_trichotomy N₁ N₂ with (H | rfl | H)
exacts [⟨N₁, fun j hj => (lt_N₁ _ hj).trans (lt_N₂ _ <| hj.trans H), lt_N₂ _ H ▸ a_lt_b⟩,
⟨N₁, fun j hj => (lt_N₁ _ hj).trans (lt_N₂ _ hj), a_lt_b.trans b_lt_c⟩,
⟨N₂, fun j hj => (lt_N₁ _ (hj.trans H)).trans (lt_N₂ _ hj), (lt_N₁ _ H).symm ▸ b_lt_c⟩]
