English
Let x,y be maps with codomain N and domain α, and r an ordering on α with IsStrictOrder. If x < y in Lex, there exists i ∈ α such that for all j, if r j i then x j ≤ y j and y j ≤ x j, and x i < y i.
Русский
Пусть x,y ∈ α →₀ N и r — упорядочение на α с IsStrictOrder. Если x < y в Lex, существует i ∈ α, для которого для всех j с r j i выполняется x j ≤ y j и y j ≤ x j, и x i < y i.
LaTeX
$$$\\exists i \\in α,\\ (\\forall j,\\ r j i \\Rightarrow x_j \\le y_j \\land y_j \\le x_j) \\land x_i < y_i$$$
Lean4
theorem lex_lt_of_lt_of_preorder [Preorder N] (r) [IsStrictOrder α r] {x y : α →₀ N} (hlt : x < y) :
∃ i, (∀ j, r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i :=
DFinsupp.lex_lt_of_lt_of_preorder r (id hlt : x.toDFinsupp < y.toDFinsupp)
