disjSum_lt_disjSum_of_lt_of_le

Mathlib.Data.Multiset.Sum

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

← MathLib Explorer

English

If s1 < s2 and t1 ≤ t2 then s1.disjSum t1 < s2.disjSum t2.

Русский

Если s1 < s2 и t1 ≤ t2, то s1.disjSum t1 < s2.disjSum t2.

LaTeX

$$$ (s_1 < s_2) \\land (t_1 \\le t_2) \\Rightarrow s_1.disjSum t_1 < s_2.disjSum t_2 $$$

Lean4

theorem disjSum_lt_disjSum_of_lt_of_le (hs : s₁ < s₂) (ht : t₁ ≤ t₂) : s₁.disjSum t₁ < s₂.disjSum t₂ :=
  add_lt_add_of_lt_of_le (map_lt_map hs) (map_le_map ht)

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

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

Разделы

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

Аффилиация

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