covBy_cons

Mathlib.Data.Finset.Grade

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

English

For any finite set s and element a not in s, the set s is covered by insert a s.

Русский

Если a не принадлежит s, то s покрывается вставкой a в s.

LaTeX

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

Lean4

@[simp]
theorem covBy_cons (ha : a ∉ s) : s ⋖ s.cons a ha := by simp [← val_covBy_val]

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

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

Разделы

Аффилиация

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