Nuprl Definition : face-compatible
face-compatible(X;I;f1;f2) ==
let y,b,w = f1 in
let z,c,u = f2 in
(¬(y = z ∈ Cname)) ⇒ ((z:=c)(w) = (y:=b)(u) ∈ X(I-[y; z]))
Definitions occuring in Statement :
cube-set-restriction: f(s),
I-cube: X(I),
face-map: (x:=i),
cname_deq: CnameDeq,
coordinate_name: Cname,
list-diff: as-bs,
cons: [a / b],
nil: [],
spreadn: spread3,
not: ¬A,
implies: P ⇒ Q,
equal: s = t ∈ T
Definitions occuring in definition :
spreadn: spread3,
implies: P ⇒ Q,
not: ¬A,
coordinate_name: Cname,
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)
FDL editor aliases :
face-compatible
Latex:
face-compatible(X;I;f1;f2) ==
let y,b,w = f1 in
let z,c,u = f2 in
(\mneg{}(y = z)) {}\mRightarrow{} ((z:=c)(w) = (y:=b)(u))
Date html generated:
2016_06_16-PM-05_49_41
Last ObjectModification:
2015_09_23-AM-09_31_17
Theory : cubical!sets
Home
Index