mem_of_mem_erase

Mathlib.Data.Finset.Erase

URI: https://scilib.ai/kg/mathlib#Finset.mem_of_mem_erase

English

If b ∈ erase s a, then b ∈ s.

Русский

Если b ∈ erase s a, то b ∈ s.

LaTeX

$$$ b \in \mathrm{erase}(s,a) \Rightarrow b \in s $$$

Lean4

theorem mem_of_mem_erase : b ∈ erase s a → b ∈ s :=
  Multiset.mem_of_mem_erase

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

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

Разделы

Аффилиация

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