disjSum_strictMono_left

Mathlib.Data.Multiset.Sum

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

← MathLib Explorer

English

For any t, the function s ↦ s.disjSum t is strictly monotone in s.

Русский

Для любого t отображение s ↦ s.disjSum t строго монотонно по s.

LaTeX

$$$ \\text{StrictMono}(s \\mapsto s.disjSum t) $$$

Lean4

theorem disjSum_strictMono_left (t : Multiset β) : StrictMono fun s : Multiset α => s.disjSum t := fun _ _ hs =>
  disjSum_lt_disjSum_of_lt_of_le hs le_rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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