disjoint_add_right

Mathlib.Data.Multiset.UnionInter

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem disjoint_add_right {s t u : Multiset α} : Disjoint s (t + u) ↔ Disjoint s t ∧ Disjoint s u := by
  rw [_root_.disjoint_comm, disjoint_add_left]; tauto

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

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

Разделы

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

Аффилиация

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