notMem_erase

Mathlib.Data.Finset.Erase

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

English

An element cannot belong to erase s a when compared with its own value a.

Русский

Элемент не принадлежит erase s a, если сравнивать его с тем же значением a.

LaTeX

$$$ a \notin \mathrm{erase}(s,a) $$$

Lean4

theorem notMem_erase (a : α) (s : Finset α) : a ∉ erase s a :=
  s.2.notMem_erase

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

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

Разделы

Аффилиация

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