mem_erase_of_ne

Mathlib.Data.Multiset.AddSub

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

English

If a ≠ b then a ∈ s.erase b ↔ a ∈ s.

Русский

Пусть a ≠ b; тогда a принадлежит s.erase b тогда и только тогда, когда a принадлежит s.

LaTeX

$$$a \neq b \Rightarrow (a \in s.erase b \iff a \in s)$$$

Lean4

theorem mem_erase_of_ne {a b : α} {s : Multiset α} (ab : a ≠ b) : a ∈ s.erase b ↔ a ∈ s :=
  Quot.inductionOn s fun _l => List.mem_erase_of_ne ab

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

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

Разделы

Аффилиация

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