fst_snd

Mathlib.Order.GameAdd

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

English

If rα(a1,a2) then GameAdd rα s(a1,b) s(b,a2).

Русский

Если rα(a1,a2), тогда GameAdd между s(a1,b) и s(b,a2).

LaTeX

$$$\forall a_1,a_2,b:\; r_\alpha(a_1,a_2) \Rightarrow \mathrm{GameAdd}(r_\alpha,\mathrm{Sym2.mk}(a_1,b),\mathrm{Sym2.mk}(b,a_2)).$$$

Lean4

theorem fst_snd {a₁ a₂ b : α} (h : rα a₁ a₂) : GameAdd rα s(a₁, b) s(b, a₂) :=
  by
  rw [Sym2.eq_swap]
  exact GameAdd.snd h

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

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

Разделы

Аффилиация

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