Nuprl Lemma : left_indices_minus_lemma
∀G:Top. (left-indices(-(G)) ~ right-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],
left-indices: left-indices(g),
pi1: fst(t),
Game-minus: -(G),
mkGame: {mkGame(f[a] with a:L | g[b] with b:R},
Wsup: Wsup(a;b),
right-indices: right-indices(g),
pi2: snd(t)
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. (left-indices(-(G)) \msim{} right-indices(G))
Date html generated:
2019_10_31-AM-06_35_01
Last ObjectModification:
2019_09_12-PM-01_35_54
Theory : Numbers!and!Games
Home
Index