English
If each coordinate is ordered by a preorder and i obeys a strict order, then a strict lexicographic comparison on DFinsupps can be witnessed at some index i by the coordinates and the order relation.
Русский
Если в каждой координате установлен порядок preorder и существует строгий порядок по индексам, то строгий лексикографический порядок на DFinsupp достигается в некотором индексе i посредством координат и порядка.
LaTeX
$$theorem lex_lt_of_lt_of_preorder [∀ i, Preorder (α i)] (r) [IsStrictOrder ι r] {x y : Π₀ i, α i} (hlt : x < y) : ∃ i, (∀ j, r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i$$
Lean4
theorem lex_lt_of_lt_of_preorder [∀ i, Preorder (α i)] (r) [IsStrictOrder ι r] {x y : Π₀ i, α i} (hlt : x < y) :
∃ i, (∀ j, r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i :=
by
obtain ⟨hle, j, hlt⟩ := Pi.lt_def.1 hlt
classical
have : (x.neLocus y : Set ι).WellFoundedOn r := (x.neLocus y).finite_toSet.wellFoundedOn
obtain ⟨i, hi, hl⟩ := this.has_min {i | x i < y i} ⟨⟨j, mem_neLocus.2 hlt.ne⟩, hlt⟩
refine ⟨i, fun k hk ↦ ⟨hle k, ?_⟩, hi⟩
exact of_not_not fun h ↦ hl ⟨k, mem_neLocus.2 (ne_of_not_le h).symm⟩ ((hle k).lt_of_not_ge h) hk
