subRight

Mathlib.Algebra.Lie.Free

URI: https://scilib.ai/kg/mathlib#FreeLieAlgebra.Rel.subRight

English

If a and b are related, then a−c and b−c are related: Rel(R,X,a,b) ⇒ Rel(R,X,a−c,b−c).

Русский

Если a и b связаны, то a−c и b−c связаны: Rel(R,X,a,b) ⇒ Rel(R,X,a−c,b−c).

LaTeX

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

Lean4

theorem subRight {a b : lib R X} (c : lib R X) (h : Rel R X a b) : Rel R X (a - c) (b - c) := by
  simpa only [sub_eq_add_neg] using h.add_right (-c)

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

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

Разделы

Аффилиация

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