snd_fst

Mathlib.Order.GameAdd

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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