snd

Mathlib.Order.GameAdd

URI: https://scilib.ai/kg/mathlib#Sym2.GameAdd.snd

English

If rα(b1,b2) then the GameAdd relation holds between s(a,b1) and s(a,b2).

Русский

Если rα(b1,b2), то GameAdd между s(a,b1) и s(a,b2) выполняется.

LaTeX

$$$\forall a,b_1,b_2:\; r_\alpha(b_1,b_2) \Rightarrow \mathrm{GameAdd}(r_\alpha,\mathrm{Sym2.mk}(a,b_1),\mathrm{Sym2.mk}(a,b_2)).$$$

Lean4

theorem snd {a b₁ b₂ : α} (h : rα b₁ b₂) : GameAdd rα s(a, b₁) s(a, b₂) :=
  (Prod.GameAdd.snd h).to_sym2

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

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

Разделы

Аффилиация

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