single_le_iff — Mathlib

English

For all a,b in α, toDegLex(single b 1) ≤ toDegLex(single a 1) iff a ≤ b.

Русский

Для любых a,b ∈ α верно: toDegLex(single b 1) ≤ toDegLex(single a 1) тогда и только тогда, когда a ≤ b.

LaTeX

$$$\forall a,b:\alpha,\ toDegLex(\mathrm{single}(b,1)) \le toDegLex(\mathrm{single}(a,1)) \iff a \le b$$$

Lean4

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

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