down_mk — Mathlib

English

Let α be an additive type with right-cancelation and a unit 1. For indices i, j with j + 1 = i, the relation Rel in the structure down α holds between i and j.

Русский

Пусть α — добавляющее множество с правым отменяемым сложением и единицей 1. Для индексов i, j с j + 1 = i выполнено отношение Rel в down α между i и j.

LaTeX

$$$\\forall {α} [Add α] [IsRightCancelAdd α] [One α] (i j : α) (h : j + 1 = i), (down α).Rel i j$$$

Lean4

theorem down_mk {α : Type*} [Add α] [IsRightCancelAdd α] [One α] (i j : α) (h : j + 1 = i) : (down α).Rel i j :=
  down'_mk (1 : α) i j h

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