ndunion_le_add

Mathlib.Data.Multiset.FinsetOps

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

English

The ndunion of s and t is contained in the sum s + t.

Русский

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

LaTeX

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

Lean4

theorem ndunion_le_add (s t : Multiset α) : ndunion s t ≤ s + t :=
  Quot.induction_on₂ s t fun _ _ => (union_sublist_append _ _).subperm

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

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

Разделы

Аффилиация

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