erase_eq

Mathlib.Data.Finset.Basic

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

English

Equality between erase and sdifference representation holds: erase s a equals s \\ {a}.

Русский

Равенство между erase и представлением через разность: erase s a равно s \\ {a}.

LaTeX

$$$ \\forall {s : Finset \\alpha} {a : \\alpha}, erase s a = s \\\\{ a \\}$$$

Lean4

theorem erase_eq (s : Finset α) (a : α) : s.erase a = s \ { a } :=
  (sdiff_singleton_eq_erase _ _).symm

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

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

Разделы

Аффилиация

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