card_filter_le

Mathlib.Data.Finset.Card

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

English

For any s and predicate P, the cardinality of s.filter P is at most the cardinality of s.

Русский

Для любого s и предиката P кардинал s.filter P не больше кардинала s.

LaTeX

$$$\\#(s.filter P) \\le \\#s$$$

Lean4

theorem card_filter_le (s : Finset α) (p : α → Prop) [DecidablePred p] : #(s.filter p) ≤ #s :=
  card_le_card <| filter_subset _ _

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

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

Разделы

Аффилиация

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