disjoint_add_left

Mathlib.Data.Multiset.UnionInter

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

← MathLib Explorer

English

Disjoint (s + t) u iff Disjoint s u and Disjoint t u.

Русский

Непересечение (s + t) с u эквивалентно тому, что Disjoint s u и Disjoint t u.

LaTeX

$$$ \\mathrm{Disjoint}(s + t, u) \\iff \\mathrm{Disjoint}(s, u) \\land \\mathrm{Disjoint}(t, u) $$$

Lean4

@[simp]
theorem disjoint_add_left {s t u : Multiset α} : Disjoint (s + t) u ↔ Disjoint s u ∧ Disjoint t u := by
  simp [disjoint_left, or_imp, forall_and]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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