sub_congr

Mathlib.SetTheory.PGame.Algebra

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

English

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

Русский

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

LaTeX

$$$ (w \\approx x) \\ (y \\approx z) \\Rightarrow (w - y \\approx x - z) $$$

Lean4

theorem sub_congr {w x y z : PGame} (h₁ : w ≈ x) (h₂ : y ≈ z) : w - y ≈ x - z :=
  add_congr h₁ (neg_equiv_neg_iff.2 h₂)

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

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

Разделы

Аффилиация

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