count_one

Mathlib.Data.Nat.Count

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

English

For any predicate p, count p 1 equals 1 if p 0 holds and 0 otherwise.

Русский

Для любого p count p 1 равно 1, если p 0 истинно, иначе 0.

LaTeX

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

Lean4

theorem count_one : count p 1 = if p 0 then 1 else 0 := by simp [count_succ]

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

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

Разделы

Аффилиация

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