sub_congr_right

Mathlib.SetTheory.PGame.Algebra

URI: https://scilib.ai/kg/mathlib#SetTheory.PGame.sub_congr_right

English

If y is equivalent to z, then x minus y is equivalent to x minus z.

Русский

Если y эквивалентен z, то x − y эквивалентен x − z.

LaTeX

$$$ (h:\\, y \\approx z) \\Rightarrow (x - y \\approx x - z) $$$

Lean4

theorem sub_congr_right {x y z : PGame} : (y ≈ z) → (x - y ≈ x - z) :=
  sub_congr equiv_rfl

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

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

Разделы

Аффилиация

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