card_add_card_compl

Mathlib.Data.Fintype.Card

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

← MathLib Explorer

English

The sum of the cardinalities equals the cardinality of α: |s| + |s^c| = |α|.

Русский

Сумма кардиналов равна кардиналу α: |s| + |s^c| = |α|.

LaTeX

$$|s| + |s^c| = |\alpha|$$

Lean4

@[simp]
theorem card_add_card_compl [DecidableEq α] [Fintype α] (s : Finset α) : #s + #sᶜ = Fintype.card α := by
  rw [Finset.card_compl, ← Nat.add_sub_assoc (card_le_univ s), Nat.add_sub_cancel_left]

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

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

Разделы

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

Аффилиация

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