even_iff_imp

Mathlib.Data.Fin.Parity

URI: https://scilib.ai/kg/mathlib#Fin.even_iff_imp

English

Even k is equivalent to saying that if n is even then k.val is even.

Русский

Четность k равна условию, что если n четно, то k.val четен.

LaTeX

$$$\mathrm{Even}(k) \iff (\mathrm{Even}(n) \rightarrow \mathrm{Even}(k.\mathrm{val})).$$$

Lean4

theorem even_iff_imp : Even k ↔ (Even n → Even k.val) :=
  by
  rw [imp_iff_not_or, Nat.not_even_iff_odd]
  exact even_iff

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

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

Разделы

Аффилиация

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