single_antitone

Mathlib.Data.Finsupp.MonomialOrder.DegLex

URI: https://scilib.ai/kg/mathlib#Finsupp.DegLex.single_antitone

English

The map a ↦ toDegLex(single a 1) is antitone with respect to α.

Русский

Отображение a ↦ toDegLex(single a 1) антонолитно по отношению к α.

LaTeX

$$$\text{Antitone}\left(a \mapsto \mathrm{toDegLex}(\mathrm{single}(a,1))\right)$$$

Lean4

theorem single_antitone : Antitone (fun (a : α) ↦ toDegLex (single a 1)) :=
  single_strictAnti.antitone

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

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

Разделы

Аффилиация

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