instDecidablePredOdd — Mathlib

English

The predicate 'n is odd' is decidable for integers; equivalently, for every n, Odd(n) or not Odd(n) holds.

Русский

Предикат 'нечетность' для целых чисел разрешим; то есть для каждого n выполняется либо Odd(n), либо не Odd(n).

LaTeX

$$$\\forall n \\in \\mathbb{Z}, \\ Odd(n) \\lor \\lnot Odd(n)$$$

Lean4

instance : DecidablePred (Odd : ℤ → Prop) := fun _ => decidable_of_iff _ not_even_iff_odd

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