Nuprl Definition : face-lattice-tube
face-lattice-tube(I;phi;j) == s(phi) ∨ (j=0) ∨ (j=1)
Definitions occuring in Statement :
face-presheaf: 𝔽,
fl1: (x=1),
fl0: (x=0),
face_lattice: face_lattice(I),
cube-set-restriction: f(s),
nc-s: s,
add-name: I+i,
lattice-join: a ∨ b
Definitions occuring in definition :
cube-set-restriction: f(s),
face-presheaf: 𝔽,
nc-s: s,
lattice-join: a ∨ b,
face_lattice: face_lattice(I),
add-name: I+i,
fl0: (x=0),
fl1: (x=1)
FDL editor aliases :
face-lattice-tube
Latex:
face-lattice-tube(I;phi;j) == s(phi) \mvee{} (j=0) \mvee{} (j=1)
Date html generated:
2016_05_18-PM-00_19_37
Last ObjectModification:
2016_02_03-PM-06_03_10
Theory : cubical!type!theory
Home
Index