Nuprl Definition : I-face
I-face(X;I) == x:nameset(I) × ℕ2 × X(I-[x])
Definitions occuring in Statement :
I-cube: X(I),
nameset: nameset(L),
cname_deq: CnameDeq,
list-diff: as-bs,
cons: [a / b],
nil: [],
int_seg: {i..j-},
product: x:A × B[x],
natural_number: $n
Definitions occuring in definition :
nameset: nameset(L),
product: x:A × B[x],
int_seg: {i..j-},
natural_number: $n,
I-cube: X(I),
list-diff: as-bs,
cname_deq: CnameDeq,
cons: [a / b],
nil: []
FDL editor aliases :
I-face
Latex:
I-face(X;I) == x:nameset(I) \mtimes{} \mBbbN{}2 \mtimes{} X(I-[x])
Date html generated:
2016_06_16-PM-05_48_27
Last ObjectModification:
2015_09_23-AM-09_31_00
Theory : cubical!sets
Home
Index