English
If x < y in DFinsupp under a family of partial orders, then the Lex order agrees with the coordinatewise order via Pi.Lex.
Русский
Если x < y в DFinsupp по семейству частичных порядков, то порядок Lex согласуется с покоординатным порядком через Pi.Lex.
LaTeX
$$theorem lex_lt_of_lt [∀ i, PartialOrder (α i)] (r) [IsStrictOrder ι r] {x y : DFinsupp fun i => α i} (hlt : x < y) : Pi.Lex r (fun {i} x1 x2 => (inst_1 i).lt x1 x2) (coeff x) (coeff y)$$
Lean4
theorem lex_lt_of_lt [∀ i, PartialOrder (α i)] (r) [IsStrictOrder ι r] {x y : Π₀ i, α i} (hlt : x < y) :
Pi.Lex r (· < ·) x y := by
simp_rw [Pi.Lex, le_antisymm_iff]
exact lex_lt_of_lt_of_preorder r hlt
