count_iff_forall_not

Mathlib.Data.Nat.Count

URI: https://scilib.ai/kg/mathlib#Nat.count_iff_forall_not

English

Count p n equals 0 if and only if p(k) is false for all k < n.

Русский

count(p,n) = 0 тогда и только если p(k) ложь для всех k < n.

LaTeX

$$$\operatorname{count}(p,n) = 0 \iff \forall k < n,\; \neg p(k)$$$

Lean4

theorem count_iff_forall_not {n : ℕ} : count p n = 0 ↔ ∀ m < n, ¬p m := by simp [count_eq_card_filter_range]

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

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

Разделы

Аффилиация

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