fst

Mathlib.Order.GameAdd

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

English

If rα(a1,a2) then the GameAdd relation holds between s(a1,b) and s(a2,b).

Русский

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

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}(a_2,b)).$$$

Lean4

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

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

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

Разделы

Аффилиация

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