disjoint_union_left

Mathlib.Data.Multiset.UnionInter

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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