countP_eq_zero

Mathlib.Data.Multiset.Count

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

English

countP p s = 0 iff for all a in s, not p a.

Русский

countP p s = 0 ⇔ для всех a ∈ s верно ¬p a.

LaTeX

$$$\operatorname{countP}(p, s) = 0 \iff \forall a \in s, \neg p(a)$$$

Lean4

theorem countP_eq_zero {s} : countP p s = 0 ↔ ∀ a ∈ s, ¬p a :=
  Quot.inductionOn s fun _l => by simp [List.countP_eq_zero]

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

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

Разделы

Аффилиация

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