count_succ_eq_succ_count_iff

Mathlib.Data.Nat.Count

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

English

For any p, count p (n+1) equals count p n if and only if p n is false.

Русский

Для любого p, count p (n+1) = count p n тогда и только тогда, когда p(n) ложно.

LaTeX

$$$$\operatorname{count}(p, n+1) = \operatorname{count}(p, n) \iff \neg p(n).$$$$

Lean4

theorem count_succ_eq_succ_count_iff {n : ℕ} : count p (n + 1) = count p n + 1 ↔ p n := by grind

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

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

Разделы

Аффилиация

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