Nuprl Definition : function def
x:A ⟶ B[x] == PRIMITIVE
Rules referencing :
atom_eqEquality,
int_eqEquality,
functionEquality,
lambdaFormation,
lambdaEquality,
dependent_functionElimination,
functionUniverseElim,
applyEquality,
functionExtensionality,
independent_functionElimination,
lessEquality,
barInduction,
bar_Induction,
strong_bar_Induction,
Continuity,
StrongContinuity2,
classicalIntroduction,
int_eqReduceFalseSq,
atomn_eqReduceFalseSq,
atom_eqReduceFalseSq,
atomn_eqEquality,
freeFromAtomApplication
FDL editor aliases :
dfun
Latex:
x:A {}\mrightarrow{} B[x] == PRIMITIVE
Date html generated:
2016_05_13-PM-03_03_56
Last ObjectModification:
2006_01_26-PM-03_54_22
Theory : core_1
Home
Index