count_ne_iff_exists

Mathlib.Data.Nat.Count

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

English

The nonzero count condition is equivalent to the existence of a witness below n.

Русский

Не нулевость счёта эквивалентна существованию некоторого m < n с p(m).

LaTeX

$$$\operatorname{count}(p,n) \neq 0 \iff \exists m < n,\; p(m)$$$

Lean4

theorem count_ne_iff_exists {n : ℕ} : n.count p ≠ 0 ↔ ∃ m < n, p m := by simp [Nat.count_iff_forall_not]

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

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

Разделы

Аффилиация

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