single_le_iff — Mathlib

English

For all a,b in α, toLex(single b 1) ≤ toLex(single a 1) if and only if a ≤ b.

Русский

Для любых a,b ∈ α, toLex(single b 1) ≤ toLex(single a 1) тогда и только тогда, когда a ≤ b.

LaTeX

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

Lean4

theorem single_le_iff {a b : α} : toLex (single b 1) ≤ toLex (single a 1) ↔ a ≤ b :=
  Lex.single_strictAnti.le_iff_ge

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