Nuprl Definition : product def
x:A × B[x] == PRIMITIVE
Rules referencing :
productEquality,
dependent_pairFormation,
dependent_pairEquality,
productElimination,
productUniverseElim,
spreadEquality,
independent_pairFormation,
independent_pairEquality,
equalityEqualityBase,
callbyvalueSpread,
spreadExceptionCases
FDL editor aliases :
dprod
Latex:
x:A \mtimes{} B[x] == PRIMITIVE
Date html generated:
2016_05_13-PM-03_03_53
Last ObjectModification:
2006_01_26-PM-03_54_18
Theory : core_1
Home
Index