disjSum_mono

Mathlib.Data.Multiset.Sum

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

English

If s1 ≤ s2 and t1 ≤ t2 as multisets, then s1.disjSum t1 ≤ s2.disjSum t2.

Русский

Если s1 ≤ s2 и t1 ≤ t2 как мультимножества, то s1.disjSum t1 ≤ s2.disjSum t2.

LaTeX

$$$ s_1 \\disjSum t_1 \\le s_2 \\disjSum t_2 $$$

Lean4

theorem disjSum_mono (hs : s₁ ≤ s₂) (ht : t₁ ≤ t₂) : s₁.disjSum t₁ ≤ s₂.disjSum t₂ :=
  add_le_add (map_le_map hs) (map_le_map ht)

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

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

Разделы

Аффилиация

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