DFinsupp.lex_lt_of_lt_of_preorder

theorem DFinsupp.lex_lt_of_lt_of_preorder : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : (i : ι) → Preorder (α i)] (r : ι → ι → Prop) [inst_2 : IsStrictOrder ι r] {x y : Π₀ (i : ι), α i}, x < y → ∃ i, (∀ (j : ι), r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i

This theorem states that for any types ι and α (which is dependent on ι), equipped with a zero structure and a preorder on α, and a strict order on ι, if we have two elements 'x' and 'y' of the direct-sum type of α, and 'x' is strictly less than 'y', then there exists an index 'i' such that for all indices 'j' that are strictly less than 'i' according to order 'r', the component of 'x' at 'j' is less than or equal to the component of 'y' at 'j' and the component of 'y' at 'j' is less than or equal to the component of 'x' at 'j', and the component of 'x' at 'i' is strictly less than the component of 'y' at 'i'. In other words, it provides a condition for the lexicographic order of elements in a direct-sum type.

More concisely: Given types ι and α with zero structures and preorders, and a strict order on ι, if 'x' and 'y' are elements of the direct sum of α, and 'x' is strictly less than 'y' according to the lexicographic order induced by the strict order on ι and the component-wise preorder on α, then there exists an index 'i' such that the component of 'x' at 'i' is strictly less than the component of 'y' at 'i'.