Nuprl Definition : A-open-box
A-open-box(X;A;I;alpha;J;x;i) ==
{L:A-face(X;A;I;alpha) List|
A-adjacent-compatible(X;A;I;alpha;L)
∧ (¬(x ∈ J))
∧ l_subset(Cname;J;I)
∧ ((∀y:nameset(J). ∀c:ℕ2. (∃f∈L. A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2)))
∧ (∃f∈L. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
∧ (∀f∈L.¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2))))
∧ (∀f∈L.(fst(f) ∈ [x / J]))
∧ (∀f1,f2∈L. ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))}
Definitions occuring in Statement :
A-adjacent-compatible: A-adjacent-compatible(X;A;I;alpha;L),
A-face-name: A-face-name(f),
A-face: A-face(X;A;I;alpha),
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,
A-face: A-face(X;A;I;alpha),
A-adjacent-compatible: A-adjacent-compatible(X;A;I;alpha;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,
A-face-name: A-face-name(f)
FDL editor aliases :
A-open-box
Latex:
A-open-box(X;A;I;alpha;J;x;i) ==
\{L:A-face(X;A;I;alpha) List|
A-adjacent-compatible(X;A;I;alpha;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. A-face-name(f) = <y, c>))
\mwedge{} (\mexists{}f\mmember{}L. A-face-name(f) = <x, i>)
\mwedge{} (\mforall{}f\mmember{}L.\mneg{}(A-face-name(f) = <x, 1 - i>)))
\mwedge{} (\mforall{}f\mmember{}L.(fst(f) \mmember{} [x / J]))
\mwedge{} (\mforall{}f1,f2\mmember{}L. \mneg{}(A-face-name(f1) = A-face-name(f2)))\}
Date html generated:
2016_06_16-PM-05_56_16
Last ObjectModification:
2015_09_23-AM-09_31_47
Theory : cubical!sets
Home
Index