union_le_union_left

Mathlib.Data.Multiset.UnionInter

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

English

If s ≤ t, then for any u, u ∪ s ≤ u ∪ t.

Русский

Если s ≤ t, то для любого u выполняется u ∪ s ≤ u ∪ t.

LaTeX

$$$\\forall s,t,u \\in \\mathrm{Multiset}(\\alpha),\\ s \\le t \\Rightarrow u \\cup s \\le u \\cup t.$$$

Lean4

@[gcongr]
theorem union_le_union_left (h : s ≤ t) (u) : u ∪ s ≤ u ∪ t :=
  sup_le_sup_left h _

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

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

Разделы

Аффилиация

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