lex_lt_iff

Mathlib.Data.Finsupp.MonomialOrder

URI: https://scilib.ai/kg/mathlib#MonomialOrder.lex_lt_iff

English

The strict lexicographic order on Finsupp corresponds to the strict less-than on the toSyn images.

Русский

Строгий лексикографический порядок на Finsupp соответствует строгому $ < $ на образах toSyn.

LaTeX

$$$$ c \\prec_{lex} d \\iff toSyn(c) < toSyn(d). $$$$

Lean4

theorem lex_lt_iff [WellFoundedGT σ] {c d : σ →₀ ℕ} : c ≺[lex] d ↔ toLex c < toLex d :=
  Iff.rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru