wcovBy_insert

Mathlib.Data.Finset.Grade

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

English

For any Finset s and element a, inserting a into s yields a WCovBy relation: s ⩿ insert a s.

Русский

Для любого Finset s и элемента a вставка a в s образует отношение WCovBy: s ⩿ insert a s.

LaTeX

$$$ s \nrightarrow insert(a,s) $$$

Lean4

@[simp]
theorem wcovBy_insert (s : Finset α) (a : α) : s ⩿ insert a s := by simp [← coe_wcovBy_coe]

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

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

Разделы

Аффилиация

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