countP_eq_card_filter

Mathlib.Data.Multiset.Filter

URI: https://scilib.ai/kg/mathlib#Multiset.countP_eq_card_filter

English

For any p, the countP p s equals the card of the filtered s by p.

Русский

Для любого p величина countP p s равна кардиналу множества s после фильтрации по p.

LaTeX

$$$\operatorname{countP} p s = \operatorname{card}(\operatorname{filter} p s)$$$

Lean4

theorem countP_eq_card_filter (s) : countP p s = card (filter p s) :=
  Quot.inductionOn s fun l => l.countP_eq_length_filter (p := (p ·))

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

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

Разделы

Аффилиация

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