Nuprl Definition : dual-plane-primitives
DualPlanePrimitives == "V":Type"S":self."V" ⟶ self."V" ⟶ ℙ"P":self."V" ⟶ self."V" ⟶ ℙ
Definitions occuring in Statement :
record-select: r.x
,
record+: record+,
record: record(x.T[x])
,
top: Top
,
prop: ℙ
,
function: x:A ⟶ B[x]
,
token: "$token"
,
universe: Type
Definitions occuring in definition :
prop: ℙ
,
token: "$token"
,
record-select: r.x
,
function: x:A ⟶ B[x]
,
universe: Type
,
top: Top
,
record: record(x.T[x])
,
record+: record+
FDL editor aliases :
dual-plane-primitives
Latex:
DualPlanePrimitives == "V":Type"S":self."V" {}\mrightarrow{} self."V" {}\mrightarrow{} \mBbbP{}"P":self."V" {}\mrightarrow{} self."V" {}\mrightarrow{} \mBbbP{}
Date html generated:
2018_05_21-PM-09_44_20
Last ObjectModification:
2018_05_09-AM-11_24_34
Theory : matrices
Home
Index