Nuprl Definition : open_box
open_box(X;I;J;x;i) ==
{L:I-face(X;I) List|
adjacent-compatible(X;I;L)
∧ (¬(x ∈ J))
∧ l_subset(Cname;J;I)
∧ ((∀y:nameset(J). ∀c:ℕ2. (∃f∈L. face-name(f) = <y, c> ∈ (nameset(I) × ℕ2)))
∧ (∃f∈L. face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
∧ (∀f∈L.¬(face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2))))
∧ (∀f∈L.(fst(f) ∈ [x / J]))
∧ (∀f1,f2∈L. ¬(face-name(f1) = face-name(f2) ∈ (nameset(I) × ℕ2)))}
Definitions occuring in Statement :
adjacent-compatible: adjacent-compatible(X;I;L),
face-name: face-name(f),
I-face: I-face(X;I),
nameset: nameset(L),
coordinate_name: Cname,
pairwise: (∀x,y∈L. P[x; y]),
l_subset: l_subset(T;as;bs),
l_exists: (∃x∈L. P[x]),
l_all: (∀x∈L.P[x]),
l_member: (x ∈ l),
cons: [a / b],
list: T List,
int_seg: {i..j-},
pi1: fst(t),
all: ∀x:A. B[x],
not: ¬A,
and: P ∧ Q,
set: {x:A| B[x]} ,
pair: <a, b>,
product: x:A × B[x],
subtract: n - m,
natural_number: $n,
equal: s = t ∈ T
Definitions occuring in definition :
set: {x:A| B[x]} ,
list: T List,
I-face: I-face(X;I),
adjacent-compatible: adjacent-compatible(X;I;L),
l_subset: l_subset(T;as;bs),
all: ∀x:A. B[x],
l_exists: (∃x∈L. P[x]),
pair: <a, b>,
subtract: n - m,
and: P ∧ Q,
l_all: (∀x∈L.P[x]),
l_member: (x ∈ l),
pi1: fst(t),
cons: [a / b],
coordinate_name: Cname,
pairwise: (∀x,y∈L. P[x; y]),
not: ¬A,
equal: s = t ∈ T,
product: x:A × B[x],
nameset: nameset(L),
int_seg: {i..j-},
natural_number: $n,
face-name: face-name(f)
FDL editor aliases :
open_box
Latex:
open\_box(X;I;J;x;i) ==
\{L:I-face(X;I) List|
adjacent-compatible(X;I;L)
\mwedge{} (\mneg{}(x \mmember{} J))
\mwedge{} l\_subset(Cname;J;I)
\mwedge{} ((\mforall{}y:nameset(J). \mforall{}c:\mBbbN{}2. (\mexists{}f\mmember{}L. face-name(f) = <y, c>))
\mwedge{} (\mexists{}f\mmember{}L. face-name(f) = <x, i>)
\mwedge{} (\mforall{}f\mmember{}L.\mneg{}(face-name(f) = <x, 1 - i>)))
\mwedge{} (\mforall{}f\mmember{}L.(fst(f) \mmember{} [x / J]))
\mwedge{} (\mforall{}f1,f2\mmember{}L. \mneg{}(face-name(f1) = face-name(f2)))\}
Date html generated:
2016_06_16-PM-05_54_06
Last ObjectModification:
2015_09_23-AM-09_31_42
Theory : cubical!sets
Home
Index