Nuprl Definition : mkGame
{mkGame(f[a] with a:L | g[b] with b:R} == Wsup(<L, R>;λx.case x of inl(a) => f[a] | inr(b) => g[b])
Definitions occuring in Statement :
Wsup: Wsup(a;b),
lambda: λx.A[x],
pair: <a, b>,
decide: case b of inl(x) => s[x] | inr(y) => t[y]
Definitions occuring in definition :
Wsup: Wsup(a;b),
pair: <a, b>,
lambda: λx.A[x],
decide: case b of inl(x) => s[x] | inr(y) => t[y]
FDL editor aliases :
mkGame
Latex:
\{mkGame(f[a] with a:L | g[b] with b:R\} == Wsup(<L, R>\mlambda{}x.case x of inl(a) => f[a] | inr(b) => g[b])
Date html generated:
2018_05_22-PM-09_52_42
Last ObjectModification:
2018_02_14-PM-09_42_36
Theory : Numbers!and!Games
Home
Index