Nuprl Definition : is-face
is-face(X;I;bx;f) == (dimension(f):=direction(f))(bx) = cube(f) ∈ X(I-[dimension(f)])
Definitions occuring in Statement :
face-cube: cube(f),
face-direction: direction(f),
face-dimension: dimension(f),
cube-set-restriction: f(s),
I-cube: X(I),
face-map: (x:=i),
cname_deq: CnameDeq,
list-diff: as-bs,
cons: [a / b],
nil: [],
equal: s = t ∈ T
Definitions occuring in definition :
equal: s = t ∈ T,
I-cube: X(I),
cube-set-restriction: f(s),
list-diff: as-bs,
cname_deq: CnameDeq,
cons: [a / b],
nil: [],
face-map: (x:=i),
face-dimension: dimension(f),
face-direction: direction(f),
face-cube: cube(f)
FDL editor aliases :
is-face
Latex:
is-face(X;I;bx;f) == (dimension(f):=direction(f))(bx) = cube(f)
Date html generated:
2016_06_16-PM-05_50_38
Last ObjectModification:
2015_09_23-AM-09_31_27
Theory : cubical!sets
Home
Index