cons_inter_of_neg

Mathlib.Data.Multiset.UnionInter

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

← MathLib Explorer

English

If a ∉ t, then (a :: s) ∩ t = s ∩ t.

Русский

Если a не принадлежит t, то (a :: s) ∩ t = s ∩ t.

LaTeX

$$$a \\notin t \\Rightarrow (a :: s) \\cap t = s \\cap t.$$$

Lean4

@[simp]
theorem cons_inter_of_neg (s : Multiset α) : a ∉ t → (a ::ₘ s) ∩ t = s ∩ t :=
  Quotient.inductionOn₂ s t fun _l₁ _l₂ h => congr_arg ofList <| cons_bagInter_of_neg _ h

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

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

Разделы

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

Аффилиация

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