add_congr

Mathlib.SetTheory.PGame.Algebra

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

← MathLib Explorer

English

For all w,x,y,z, w ≈ x and y ≈ z imply w + y ≈ x + z.

Русский

Для всех w,x,y,z; если w ≈ x и y ≈ z, то w + y ≈ x + z.

LaTeX

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

Lean4

theorem add_congr {w x y z : PGame} (h₁ : w ≈ x) (h₂ : y ≈ z) : w + y ≈ x + z :=
  ⟨(add_le_add_left h₂.1 w).trans (add_le_add_right h₁.1 z), (add_le_add_left h₂.2 x).trans (add_le_add_right h₁.2 y)⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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