Nuprl Definition : injectively-presented
InjectivelyPresented(s) == Inj(set-dom(s);Set{i:l};λx.set-item(s;x))
Definitions occuring in Statement :
set-item: set-item(s;x),
set-dom: set-dom(s),
Set: Set{i:l},
inject: Inj(A;B;f),
lambda: λx.A[x]
Definitions occuring in definition :
set-item: set-item(s;x),
lambda: λx.A[x],
Set: Set{i:l},
set-dom: set-dom(s),
inject: Inj(A;B;f)
FDL editor aliases :
inj-presd
Latex:
InjectivelyPresented(s) == Inj(set-dom(s);Set\{i:l\};\mlambda{}x.set-item(s;x))
Date html generated:
2018_05_29-PM-01_55_07
Last ObjectModification:
2018_05_24-PM-09_55_25
Theory : constructive!set!theory
Home
Index