instAddLeftMono

Mathlib.Algebra.Order.Group.Multiset

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

English

Addition on the left is monotone: if s ≤ t then a + s ≤ a + t.

Русский

Сложение слева монотонно по отношению к правой части: если s ≤ t, то a + s ≤ a + t.

LaTeX

$$$ s \le t \implies a + s \le a + t $$$

Lean4

instance instAddLeftMono : AddLeftMono (Multiset α) where elim _s _t _u := Multiset.add_le_add_left

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

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

Разделы

Аффилиация

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