erase_wcovBy

Mathlib.Data.Finset.Grade

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

English

For any Finset s and element a, s.erase a WCovBy s.

Русский

Для любого Finset s и элемента a, s.erase a WCovBy s.

LaTeX

$$$ s.erase a \; ⩿ \; s $$$

Lean4

@[simp]
theorem erase_wcovBy (s : Finset α) (a : α) : s.erase a ⩿ s := by simp [← coe_wcovBy_coe]

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

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

Разделы

Аффилиация

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