nonMemberSubfamily

Mathlib.Combinatorics.SetFamily.Compression.Down

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

English

The subfamily of 𝒜 consisting of those members not containing a.

Русский

Подсемейство 𝒜, состоящее из элементов, не содержащих a.

LaTeX

$$$\operatorname{nonMemberSubfamily}(a, 𝒜) = \{ s \in 𝒜 \mid a \notin s \ \}$$$

Lean4

/-- Elements of `𝒜` that do not contain `a`. -/
def nonMemberSubfamily (a : α) (𝒜 : Finset (Finset α)) : Finset (Finset α) :=
  {s ∈ 𝒜 | a ∉ s}

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

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

Разделы

Аффилиация

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