odd_add_one_iff_even — Mathlib

English

Let n be a positive natural number and k be an element of Fin(n); then k+1 is odd if and only if k is even.

Русский

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

LaTeX

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

Lean4

theorem odd_add_one_iff_even [NeZero n] : Odd (k + 1) ↔ Even k :=
  ⟨fun ⟨k, hk⟩ ↦ add_right_cancel hk ▸ even_two_mul k, Even.add_one⟩

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