even_add_one_iff_odd — Mathlib

English

Let n be a positive natural number and k ∈ Fin(n). Then k+1 is even if and only if k is odd.

Русский

Пусть n — положительное натуральное число и k ∈ Fin(n). Тогда k+1 чётно тогда и только тогда, когда k нечётно.

LaTeX

$$$\forall {n}\,(\forall k\in\mathrm{Fin}(n))\;\big(\operatorname{Even}(k+1) \iff \operatorname{Odd}(k)\big).$$$

Lean4

theorem even_add_one_iff_odd [NeZero n] : Even (k + 1) ↔ Odd k :=
  ⟨fun ⟨k, hk⟩ ↦ eq_sub_iff_add_eq.mpr hk ▸ (Even.add_self k).sub_odd odd_one, Odd.add_one⟩

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