cons_inter_of_pos

Mathlib.Data.Multiset.UnionInter

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

← MathLib Explorer

English

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

Русский

Если a ∈ t, то (a :: s) ∩ t = a :: (s ∩ (t.erase a)).

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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