nonMemberSubfamily_memberSubfamily

Mathlib.Combinatorics.SetFamily.Compression.Down

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

English

(𝒜.nonMemberSubfamily a).memberSubfamily a = 𝒜.memberSubfamily a.

Русский

(𝒜.nonMemberSubfamily a).memberSubfamily a = 𝒜.memberSubfamily a.

LaTeX

$$$ (𝒜.nonMemberSubfamily(a)).memberSubfamily(a) = 𝒜.memberSubfamily(a) $$$

Lean4

@[simp]
theorem nonMemberSubfamily_memberSubfamily : (𝒜.memberSubfamily a).nonMemberSubfamily a = 𝒜.memberSubfamily a :=
  by
  ext
  simp

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

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

Разделы

Аффилиация

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