down'_mk — Mathlib

English

In an additive type α with right-cancelation, for any a, i, j with j + a = i, the relation Rel in the type down' a between i and j holds.

Русский

В добавочном типе α с правым отменяемым сложением для любых a, i, j, если j + a = i, то выполняется отношение Rel в down' a между i и j.

LaTeX

$$$\\forall {α} [Add α] [IsRightCancelAdd α] (a i j : α), \\; h : j + a = i \\Rightarrow (down' a).Rel i j$$$

Lean4

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

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