toLex_le_toLex — Mathlib

English

If α is a type with LT and LE, then in the lexicographic order on Lex(NonemptyInterval α), we have: toLex x ≤ toLex y iff y.fst < x.fst or (x.fst = y.fst and x.snd ≤ y.snd).

Русский

Пусть α упорядочен по LT и LE. В лексикографическом порядке на Lex(NonemptyInterval α) имеем: toLex x ≤ toLex y тогда и только тогда, когда y.fst < x.fst или (x.fst = y.fst и x.snd ≤ y.snd).

LaTeX

$$$ toLex(x) \le toLex(y) \iff y.fst < x.fst \lor (x.fst = y.fst \\land x.snd \le y.snd) $$$

Lean4

theorem toLex_le_toLex {x y : NonemptyInterval α} : toLex x ≤ toLex y ↔ y.fst < x.fst ∨ x.fst = y.fst ∧ x.snd ≤ y.snd :=
  Prod.lex_def

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