up_nat_odd_add

Mathlib.Algebra.Homology.AlternatingConst

URI: https://scilib.ai/kg/mathlib#ComplexShape.up_nat_odd_add

English

If i and j are related by the up relation (i related to j by the upward shift), then i+j is odd.

Русский

Если i и j связаны отношением вверх, то сумма i+j нечётна.

LaTeX

$$$(\mathrm{ComplexShape}.up \ \mathbb{N}).Rel(i,j) \Rightarrow \operatorname{Odd}(i+j)$$$

Lean4

theorem up_nat_odd_add {i j : ℕ} (h : (ComplexShape.up ℕ).Rel i j) : Odd (i + j) :=
  by
  subst h
  norm_num

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

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

Разделы

Аффилиация

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