down_nat_odd_add

Mathlib.Algebra.Homology.AlternatingConst

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

English

If i and j are related by the down relation, then i+j is odd.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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