zero_disjoint

Mathlib.Data.Multiset.UnionInter

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

English

Disjoint 0 l for any multiset l.

Русский

Непересечение нуля с любым мультимножеством l.

LaTeX

$$$ \\mathrm{Disjoint}(0, l) $$$

Lean4

@[simp]
theorem zero_disjoint (l : Multiset α) : Disjoint 0 l :=
  disjoint_bot_left

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

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

Разделы

Аффилиация

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