even_or_odd'

Mathlib.Algebra.Ring.Parity

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

English

For every n there exists k with n = 2k or n = 2k + 1.

Русский

Для каждого n существует k, такое что n = 2k или n = 2k + 1.

LaTeX

$$$\\forall n \\in \\mathbb{N}, \\exists k \\in \\mathbb{N}, 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