addLeft — Mathlib

English

If b and c are related by h, then adding a on the left preserves the relation: if Rel(R,X,b,c) then Rel(R,X,a+b,a+c).

Русский

Если b и c связаны отношением h, то добавление слева сохраняет отношение: Rel(R,X,b,c) ⇒ Rel(R,X,a+b,a+c).

LaTeX

$$$\text{Rel}(R,X,b,c) \Rightarrow \text{Rel}(R,X,a+b,a+c)$$$

Lean4

theorem addLeft (a : lib R X) {b c : lib R X} (h : Rel R X b c) : Rel R X (a + b) (a + c) := by
  rw [add_comm _ b, add_comm _ c]; exact h.add_right _

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