card_filter

Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

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

English

For a predicate p, finite s, we have #({i ∈ s | p i}) = ∑ i∈s, ite(p i) 1 0.

Русский

Для предиката p и конечного s верно тождество: #({i ∈ s | p i}) = ∑_{i∈s} ite(p i) 1 0.

LaTeX

$$$\\#\\{i \\in s \\mid p(i)\\} = \\sum_{i \\in s} \\operatorname{ite}(p(i))\\,1\\,0$$$

Lean4

theorem card_filter (p) [DecidablePred p] (s : Finset ι) : #({i ∈ s | p i}) = ∑ i ∈ s, ite (p i) 1 0 := by
  simp [sum_ite]

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

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

Разделы

Аффилиация

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