ofIsEmpty

Mathlib.SetTheory.Game.Short

URI: https://scilib.ai/kg/mathlib#SetTheory.PGame.Short.ofIsEmpty

Lean4

/-- This leads to infinite loops if made into an instance. -/
def ofIsEmpty {l r xL xR} [IsEmpty l] [IsEmpty r] : Short (PGame.mk l r xL xR) :=
  by
  have : Fintype l := Fintype.ofIsEmpty
  have : Fintype r := Fintype.ofIsEmpty
  exact Short.mk isEmptyElim isEmptyElim

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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