Nuprl Lemma : Game_subtype
Game ⊆r (LR:GameA{i:l}() × (GameB(LR) ⟶ Game))
Proof
Definitions occuring in Statement :
Game: Game,
GameB: GameB(p),
GameA: GameA{i:l}(),
subtype_rel: A ⊆r B,
function: x:A ⟶ B[x],
product: x:A × B[x]
Definitions unfolded in proof :
ext-eq: A ≡ B,
and: P ∧ Q
Lemmas referenced :
Game_ext
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
productElimination,
thin,
hypothesis
Latex:
Game \msubseteq{}r (LR:GameA\{i:l\}() \mtimes{} (GameB(LR) {}\mrightarrow{} Game))
Date html generated:
2018_05_22-PM-09_52_19
Last ObjectModification:
2018_05_20-PM-10_36_24
Theory : Numbers!and!Games
Home
Index