disjSum_lt_disjSum_of_le_of_lt

Mathlib.Data.Multiset.Sum

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

← 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 \\le s_2) \\land (t_1 < t_2) \\Rightarrow s_1.disjSum t_1 < s_2.disjSum t_2 $$$

Lean4

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

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

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

Разделы

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

Аффилиация

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