P24

Mathlib.SetTheory.Surreal.Multiplication

URI: https://scilib.ai/kg/mathlib#Surreal.Multiplication.P24

Lean4

/-- The conjunction of P2 and P4. -/
def P24 (x₁ x₂ y : PGame) : Prop :=
  P2 x₁ x₂ y ∧ P4 x₁ x₂ y

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

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

Разделы

Аффилиация

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