fintypeRight — Mathlib

English

Every short PGame has a finite set of RightMoves.

Русский

У каждой короткой PGame конечен набор правых ходов.

LaTeX

$$$ Short(x) \Rightarrow \#(x.RightMoves) < \infty $$$

Lean4

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

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