ndunion

Mathlib.Data.Multiset.FinsetOps

URI: https://scilib.ai/kg/mathlib#Multiset.Nodup.ndunion

English

If t is nodup, then ndunion s t is nodup.

Русский

Если t без повторов, то ndunion s t без повторов.

LaTeX

$$$\\mathrm{Nodup}(t) \\Rightarrow \\mathrm{Nodup}(\\mathrm{ndunion}(s,t))$$$

Lean4

theorem ndunion (s : Multiset α) {t : Multiset α} : Nodup t → Nodup (ndunion s t) :=
  Quot.induction_on₂ s t fun _ _ => List.Nodup.union _

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

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

Разделы

Аффилиация

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