lex_le_iff_of_unique — Mathlib

English

Under Unique σ, the lexicographic non-strict order reduces to c default ≤ d default.

Русский

При Unique σ нестрогий лексикографический порядок даёт c default ≤ d default.

LaTeX

$$$$ c \\preceq_{lex} d \\iff c default \\le d default. $$$$

Lean4

theorem lex_le_iff_of_unique [Unique σ] {c d : σ →₀ ℕ} : c ≼[lex] d ↔ c default ≤ d default := by
  simp only [MonomialOrder.lex_le_iff, Finsupp.lex_le_iff_of_unique, ofLex_toLex]

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