even_or_odd'

Mathlib.Algebra.Ring.Int.Parity

URI: https://scilib.ai/kg/mathlib#Int.even_or_odd'

English

Let n be an integer. Then there exists an integer k such that n = 2k or n = 2k + 1.

Русский

Пусть n — целое число. Тогда существует целое k, такое что n = 2k или n = 2k + 1.

LaTeX

$$$\\exists k \\in \\mathbb{Z}, n = 2k \\lor n = 2k + 1$$$

Lean4

theorem even_or_odd' (n : ℤ) : ∃ k, n = 2 * k ∨ n = 2 * k + 1 := by
  simpa only [two_mul, exists_or, Odd, Even] using even_or_odd n

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

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

Разделы

Аффилиация

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