toSyn_strictMono

Mathlib.Data.Finsupp.MonomialOrder

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

English

The map toSyn is strictly monotone: it preserves strict inequality and is injective on the carrier.

Русский

Отображение toSyn строго монотонно: сохраняет строгую неравенство и инъективно на носителе.

LaTeX

$$$$ \\text{StrictMono}(m.toSyn). $$$$

Lean4

theorem toSyn_strictMono : StrictMono (m.toSyn) := by apply m.toSyn_monotone.strictMono_of_injective m.toSyn.injective

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

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

Разделы

Аффилиация

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