Nuprl Lemma : right_indices_minus_lemma
∀G:Top. (right-indices(-(G)) ~ left-indices(G))
Proof
Definitions occuring in Statement :
Game-minus: -(G),
right-indices: right-indices(g),
left-indices: left-indices(g),
top: Top,
all: ∀x:A. B[x],
sqequal: s ~ t
Definitions unfolded in proof :
all: ∀x:A. B[x],
right-indices: right-indices(g),
pi2: snd(t),
pi1: fst(t),
Game-minus: -(G),
mkGame: {mkGame(f[a] with a:L | g[b] with b:R},
Wsup: Wsup(a;b),
left-indices: left-indices(g)
Lemmas referenced :
istype-top
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
cut,
sqequalRule,
hypothesis,
introduction,
extract_by_obid
Latex:
\mforall{}G:Top. (right-indices(-(G)) \msim{} left-indices(G))
Date html generated:
2019_10_31-AM-06_35_03
Last ObjectModification:
2019_09_12-PM-01_36_58
Theory : Numbers!and!Games
Home
Index