instDecidablePredOdd

Mathlib.Algebra.Ring.Parity

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

English

There exists a decision procedure for the predicate Odd on naturals.

Русский

Существует детерминированное вычислительное решение для предиката Odd на натуральных числах.

LaTeX

$$$\exists d:\\mathbb{N} \to \{0,1\},\ \forall n,\ d(n)=1 \iff \operatorname{Odd}(n)$$$

Lean4

instance : DecidablePred (Odd : ℕ → Prop) := fun _ ↦ decidable_of_iff _ odd_iff.symm

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

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

Разделы

Аффилиация

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