single_lt_iff — Mathlib

English

For all a,b in α, the order between toLex(single b 1) and toLex(single a 1) reflects a < b exactly: toLex(single b 1) < toLex(single a 1) iff a < b.

Русский

Для любых a,b ∈ α порядок между toLex(single b 1) и toLex(single a 1) совпадает с отношением a < b: toLex(single b 1) < toLex(single a 1) тогда когда a < b.

LaTeX

$$$a,b\\in α:\\quad \\mathrm{toLex}(\\mathrm{single} b\\,1) < \\mathrm{toLex}(\\mathrm{single} a\\,1) \\iff a < b$$$

Lean4

theorem single_lt_iff {a b : α} : toLex (single b 1) < toLex (single a 1) ↔ a < b :=
  Lex.single_strictAnti.lt_iff_gt

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