singleton_disjoint

Mathlib.Data.Multiset.UnionInter

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

English

Disjoint {a} l iff a ∉ l.

Русский

Disjoint {a} l тогда и только тогда, когда a не принадлежит l.

LaTeX

$$$ \\mathrm{Disjoint}(\{a\\}, l) \\iff a \\notin l $$$

Lean4

@[simp]
theorem singleton_disjoint {l : Multiset α} {a : α} : Disjoint { a } l ↔ a ∉ l := by simp [disjoint_left]

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

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

Разделы

Аффилиация

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