fintypeLeft — Mathlib

English

Let x be a short P-game with the Left moves indexed by α. Then α must be finite.

Русский

Пусть x — короткая игра, чьи левые ходы индексируются α. Тогда множество α конечно.

LaTeX

$$$ Short\big(\langle \alpha,\beta,L,R\rangle\big) \Rightarrow \#\alpha < \infty $$$

Lean4

/-- Extracting the `Fintype` instance for the indexing type for Left's moves in a short game.
This is an unindexed typeclass, so it can't be made a global instance.
-/
def fintypeLeft {α β : Type u} {L : α → PGame.{u}} {R : β → PGame.{u}} [S : Short ⟨α, β, L, R⟩] : Fintype α := by
  cases S; assumption

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