sdiff_singleton

Mathlib.Order.UpperLower.Closure

URI: https://scilib.ai/kg/mathlib#UpperSet.sdiff_singleton

English

Removing a singleton from an upper set equals erasing that element.

Русский

Удаление элемента из верхнего множества через единичное множество эквивалентно операции удаления.

LaTeX

$$$ s.sdiff\\{a\\} = s.erase a $$$

Lean4

@[simp]
theorem sdiff_singleton (s : UpperSet α) (a : α) : s.sdiff { a } = s.erase a := by simp [sdiff, erase]

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

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

Разделы

Аффилиация

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