sum_card_slice

Mathlib.Data.Finset.Slice

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

← MathLib Explorer

English

The sum of the cardinalities of all slices equals the cardinality of 𝒜.

Русский

Сумма кардиналов всех срезов равна кардиналу 𝒜.

LaTeX

$$$ \sum_{r=0}^{|\alpha|} |(𝒜 #r)| = |𝒜| $$$

Lean4

@[simp]
theorem sum_card_slice : ∑ r ∈ Iic (Fintype.card α), #(𝒜 #r) = #𝒜 :=
  by
  letI := Classical.decEq α
  rw [← card_biUnion, biUnion_slice]
  exact Finset.pairwiseDisjoint_slice.subset (Set.subset_univ _)

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

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

Разделы

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

Аффилиация

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