count_succ

Mathlib.Data.Nat.Count

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

English

The recurrence count p (n+1) = count p n plus 1 if p n holds, else 0.

Русский

Рекуррентно: count p (n+1) = count p n плюс 1 если p(n) выполняется, иначе плюс 0.

LaTeX

$$$$\operatorname{count}(p,n+1) = \operatorname{count}(p,n) + \begin{cases}1, & p(n) \\ 0, & \neg p(n) \end{cases}.$$$$

Lean4

@[grind =]
theorem count_succ (n : ℕ) : count p (n + 1) = count p n + if p n then 1 else 0 := by grind [count, List.range_succ]

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

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

Разделы

Аффилиация

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