### 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|
\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