Nuprl Definition : irr_face
irr_face(I;as;bs) == /\(λa.(a=0)"(as) ⋃ λb.(b=1)"(bs))
Definitions occuring in Statement :
fl1: (x=1),
fl0: (x=0),
face_lattice-deq: face_lattice-deq(),
face_lattice: face_lattice(I),
names-deq: NamesDeq,
lattice-fset-meet: /\(s),
fset-image: f"(s),
fset-union: x ⋃ y,
lambda: λx.A[x]
Definitions occuring in definition :
lattice-fset-meet: /\(s),
face_lattice: face_lattice(I),
fset-union: x ⋃ y,
fl0: (x=0),
fset-image: f"(s),
names-deq: NamesDeq,
face_lattice-deq: face_lattice-deq(),
lambda: λx.A[x],
fl1: (x=1)
FDL editor aliases :
irr_face
Latex:
irr\_face(I;as;bs) == /\mbackslash{}(\mlambda{}a.(a=0)"(as) \mcup{} \mlambda{}b.(b=1)"(bs))
Date html generated:
2017_02_21-AM-10_32_51
Last ObjectModification:
2017_02_02-PM-03_08_00
Theory : cubical!type!theory
Home
Index