lex_lt_of_lt — Mathlib

English

Let α,N be as above and x,y ∈ α →₀ N with x < y in the Lex order. Then there exists i with the same property as above: for all j < i we have equality, and at i we have x_i < y_i.

Русский

Пусть x,y ∈ α →₀ N и x < y в лексикографическом порядке. Тогда существует i, для которого все более ранние координаты совпадают, а на i выполняется x_i < y_i.

LaTeX

$$$\\exists i, \\forall j,\\ r j i \\Rightarrow x_j = y_j \\land x_i < y_i$$$

Lean4

theorem lex_lt_of_lt [PartialOrder N] (r) [IsStrictOrder α r] {x y : α →₀ N} (hlt : x < y) : Pi.Lex r (· < ·) x y :=
  DFinsupp.lex_lt_of_lt r (id hlt : x.toDFinsupp < y.toDFinsupp)

Похожие утверждения