add_right — Mathlib

English

If b is related to c by the relation r, then adding the same element a on the left preserves the relation, i.e., a + b is related to a + c.

Русский

Если b связано с c отношением r, то добавление слева одинакового элемента a сохраняет отношение: a + b связано с a + c.

LaTeX

$$$\\forall a,b,c,\\, h: \\mathrm{Rel}\\ r\\ b\\ c \\Rightarrow \\mathrm{Rel}\\ r\\ (a+b)\\ (a+c).$$$

Lean4

theorem add_right {r : R → R → Prop} ⦃a b c : R⦄ (h : Rel r b c) : Rel r (a + b) (a + c) :=
  by
  rw [add_comm a b, add_comm a c]
  exact Rel.add_left h

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