countP_le_card

Mathlib.Data.Multiset.Count

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

English

For any predicate p and multiset s, countP p s ≤ card s.

Русский

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

LaTeX

$$$\operatorname{countP}(p, s) \leq \operatorname{card}(s)$$$

Lean4

theorem countP_le_card (s) : countP p s ≤ card s :=
  Quot.inductionOn s fun _l => countP_le_length (p := (p ·))

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

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

Разделы

Аффилиация

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