monotone_sym2

Mathlib.Data.Multiset.Sym

URI: https://scilib.ai/kg/mathlib#Multiset.monotone_sym2

English

The mapping m ↦ m.sym2 is monotone: m ≤ m' implies m.sym2 ≤ m'.sym2.

Русский

Отображение m ↦ m.sym2 монотонно: если m ≤ m' то m.sym2 ≤ m'.sym2.

LaTeX

$$$ m \\le m' \\Rightarrow m.sym2 \\le m'.sym2 $$$

Lean4

theorem monotone_sym2 : Monotone (Multiset.sym2 : Multiset α → _) := fun _ _ => sym2_mono

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

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

Разделы

Аффилиация

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