nat_bodd

Mathlib.Computability.Partrec

URI: https://scilib.ai/kg/mathlib#Computable.nat_bodd

English

The boolean function that tests whether a natural number is odd is computable.

Русский

Булева функция, определяющая нечётность натурального числа, вычислима.

LaTeX

$$$\mathrm{bodd}: \mathbb{N} \to \mathrm{Bool}$ is computable.$$

Lean4

theorem nat_bodd : Computable Nat.bodd :=
  Primrec.nat_bodd.to_comp

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

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

Разделы

Аффилиация

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