erase_eq_of_notMem

Mathlib.Data.Finset.Erase

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

English

If a ∉ s, then erase s a = s.

Русский

Если a ∉ s, то erase s a = s.

LaTeX

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

Lean4

@[simp]
theorem erase_eq_of_notMem {a : α} {s : Finset α} (h : a ∉ s) : erase s a = s :=
  eq_of_veq <| erase_of_notMem h

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

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

Разделы

Аффилиация

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