ndunion_le_union

Mathlib.Data.Multiset.FinsetOps

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

English

The ndunion of s and t is contained in the union s ∪ t.

Русский

Объединение ndunion(m) множества s и t содержится в объединении s ∪ t.

LaTeX

$$$\\mathrm{ndunion}(s,t) \\leq \\; s \\cup t$$$

Lean4

theorem ndunion_le_union (s t : Multiset α) : ndunion s t ≤ s ∪ t :=
  ndunion_le.2 ⟨subset_of_le le_union_left, le_union_right⟩

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

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

Разделы

Аффилиация

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