disjoint_union_right

Mathlib.Data.Multiset.UnionInter

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

English

For DecidableEq α, Disjoint s (t ∪ u) iff Disjoint s t ∧ Disjoint s u.

Русский

Для DecidableEq α, несовместность s с (t ∪ u) равносильна несовместности s t и s u.

LaTeX

$$$Disjoint s (t \\cup u) \\iff Disjoint s t \\land Disjoint s u$$$

Lean4

@[simp]
theorem disjoint_union_right [DecidableEq α] {s t u : Multiset α} : Disjoint s (t ∪ u) ↔ Disjoint s t ∧ Disjoint s u :=
  disjoint_sup_right

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

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

Разделы

Аффилиация

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