ssubsets

Mathlib.Data.Finset.Powerset

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

← MathLib Explorer

English

For a finset s, ssubsets is the finset of all strict subsets of s.

Русский

Для множества s, ssubsets есть финсет всех строгих подмножеств s.

LaTeX

$$ssubsets(s) = powerset(s) \ {s}$$

Lean4

/-- For `s` a finset, `s.ssubsets` is the finset comprising strict subsets of `s`. -/
def ssubsets (s : Finset α) : Finset (Finset α) :=
  erase (powerset s) s

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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