erase_comm

Mathlib.Data.Multiset.AddSub

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

← MathLib Explorer

English

(s.erase a).erase b = (s.erase b).erase a.

Русский

Стирание по левым аргументам коммутативно: сначала удаляем a, затем b, равно как и наоборот.

LaTeX

$$((s.erase a).erase b) = ((s.erase b).erase a)$$

Lean4

theorem erase_comm (s : Multiset α) (a b : α) : (s.erase a).erase b = (s.erase b).erase a :=
  Quot.inductionOn s fun l => congr_arg _ <| l.erase_comm a b

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

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

Разделы

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

Аффилиация

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