card_filter_eq_zero_iff

Mathlib.Data.Finset.Card

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

English

The filter is empty iff no elements satisfy P on S.

Русский

Фильтр пуст, если ни один элемент не удовлетворяет P на S.

LaTeX

$$$#(s.filter p) = 0 \\iff \\forall x \\in s, \\neg p x$$$

Lean4

theorem card_filter_eq_zero_iff {p : α → Prop} [DecidablePred p] : #(s.filter p) = 0 ↔ ∀ x ∈ s, ¬p x := by
  rw [card_eq_zero, filter_eq_empty_iff]

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

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

Разделы

Аффилиация

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