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