erase_idem

Mathlib.Order.UpperLower.Closure

URI: https://scilib.ai/kg/mathlib#LowerSet.erase_idem

English

Erasing the same element twice yields the same result as erasing once.

Русский

Повторное удаление того же элемента эквивалентно одному удалению.

LaTeX

$$$ (s.erase a).erase a = s.erase a $$$

Lean4

@[simp]
theorem erase_idem (s : LowerSet α) (a : α) : (s.erase a).erase a = s.erase a :=
  SetLike.coe_injective sdiff_idem

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

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

Разделы

Аффилиация

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