le_erase

Mathlib.Order.UpperLower.Closure

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

English

Removing an element from an upper set preserves the order relation with respect to the erase result.

Русский

Удаление элемента из верхнего множества сохраняет отношение включения относительно результата erase.

LaTeX

$$$ s \\leq s.erase a $$$

Lean4

theorem le_erase : s ≤ s.erase a :=
  diff_subset

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

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

Разделы

Аффилиация

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