Nuprl Definition : face-image
face-image(X;I;K;f;face) ==  let x,b,w = face in <f x, b, f(w)>
Definitions occuring in Statement : 
cube-set-restriction: f(s), 
cname_deq: CnameDeq, 
list-diff: as-bs, 
cons: [a / b], 
nil: [], 
spreadn: spread3, 
apply: f a, 
pair: <a, b>
Definitions occuring in definition : 
spreadn: spread3, 
pair: <a, b>, 
cube-set-restriction: f(s), 
list-diff: as-bs, 
cname_deq: CnameDeq, 
cons: [a / b], 
apply: f a, 
nil: []
FDL editor aliases : 
face-image
Latex:
face-image(X;I;K;f;face)  ==    let  x,b,w  =  face  in  <f  x,  b,  f(w)>
Date html generated:
2016_06_16-PM-05_51_10
Last ObjectModification:
2015_09_23-AM-09_31_35
Theory : cubical!sets
Home
Index