---

Step * 1 2 1 of Lemma nerve_box_label_same


1. C : SmallCategory
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. box : I-face(cubical-nerve(C);I) List
7. ∀f1,f2:I-face(cubical-nerve(C);I).
     ((f1 ∈ box)
     ⇒ (f2 ∈ box)
     ⇒ (¬(dimension(f1) = dimension(f2) ∈ Cname))
     ⇒ ((dimension(f2):=direction(f2))(cube(f1))
        = (dimension(f1):=direction(f1))(cube(f2))
        ∈ cubical-nerve(C)(I-[dimension(f1); dimension(f2)])))
8. ¬(x ∈ J)
9. l_subset(Cname;J;I)
10. ∀y:nameset(J). ∀c:ℕ2.  (∃f∈box. face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
11. (∃f∈box. face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
12. (∀f∈box.¬(face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
13. (∀f∈box.(fst(f) ∈ [x / J]))
14. (∀f1,f2∈box.  ¬(face-name(f1) = face-name(f2) ∈ (nameset(I) × ℕ2)))
15. L : name-morph(I;[])
16. ((L x) = i ∈ ℕ2) ∨ (¬↑null(J))
17. f : I-face(cubical-nerve(C);I)
18. direction(f) = (L dimension(f)) ∈ ℕ2
19. (f ∈ box)
20. v : I-face(cubical-nerve(C);I)
21. (v ∈ box)
22. direction(v) = (L dimension(v)) ∈ ℕ2
23. nerve-box-face(box;L) = v ∈ {f:I-face(cubical-nerve(C);I)| (f ∈ box) ∧ (direction(f) = (L dimension(f)) ∈ ℕ2)} 
24. ¬(dimension(v) = dimension(f) ∈ Cname)
25. (dimension(f):=direction(f))(cube(v))
= (dimension(v):=direction(v))(cube(f))
∈ cubical-nerve(C)(I-[dimension(v); dimension(f)])
⊢ (ob(cube(f)) L) = (ob(cube(v)) L) ∈ cat-ob(C)
BY
{ (MoveToConcl (-1)
   THEN (GenConclTerm ⌜cube(v)⌝⋅ THENA Auto)
   THEN (RWO "cubical-nerve-I-cube" (-2) THENA Auto)
   THEN Thin (-1)
   THEN RenameVar `F' (-1)
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜cube(f)⌝⋅ THENA Auto)
   THEN (RWO "cubical-nerve-I-cube" (-2) THENA Auto)
   THEN Thin (-1)
   THEN RenameVar `G' (-1)
   THEN MoveToConcl (-1)) }

1
1. C : SmallCategory
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. box : I-face(cubical-nerve(C);I) List
7. ∀f1,f2:I-face(cubical-nerve(C);I).
     ((f1 ∈ box)
     ⇒ (f2 ∈ box)
     ⇒ (¬(dimension(f1) = dimension(f2) ∈ Cname))
     ⇒ ((dimension(f2):=direction(f2))(cube(f1))
        = (dimension(f1):=direction(f1))(cube(f2))
        ∈ cubical-nerve(C)(I-[dimension(f1); dimension(f2)])))
8. ¬(x ∈ J)
9. l_subset(Cname;J;I)
10. ∀y:nameset(J). ∀c:ℕ2.  (∃f∈box. face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
11. (∃f∈box. face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
12. (∀f∈box.¬(face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
13. (∀f∈box.(fst(f) ∈ [x / J]))
14. (∀f1,f2∈box.  ¬(face-name(f1) = face-name(f2) ∈ (nameset(I) × ℕ2)))
15. L : name-morph(I;[])
16. ((L x) = i ∈ ℕ2) ∨ (¬↑null(J))
17. f : I-face(cubical-nerve(C);I)
18. direction(f) = (L dimension(f)) ∈ ℕ2
19. (f ∈ box)
20. v : I-face(cubical-nerve(C);I)
21. (v ∈ box)
22. direction(v) = (L dimension(v)) ∈ ℕ2
23. nerve-box-face(box;L) = v ∈ {f:I-face(cubical-nerve(C);I)| (f ∈ box) ∧ (direction(f) = (L dimension(f)) ∈ ℕ2)} 
24. ¬(dimension(v) = dimension(f) ∈ Cname)
⊢ ∀G:Functor(poset-cat(I-[dimension(f)]);C). ∀F:Functor(poset-cat(I-[dimension(v)]);C).
    (((dimension(f):=direction(f))(F)
    = (dimension(v):=direction(v))(G)
    ∈ cubical-nerve(C)(I-[dimension(v); dimension(f)]))
    ⇒ ((ob(G) L) = (ob(F) L) ∈ cat-ob(C)))

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  I  :  Cname  List
3.  J  :  nameset(I)  List
4.  x  :  nameset(I)
5.  i  :  \mBbbN{}2
6.  box  :  I-face(cubical-nerve(C);I)  List
7.  \mforall{}f1,f2:I-face(cubical-nerve(C);I).
          ((f1  \mmember{}  box)
          {}\mRightarrow{}  (f2  \mmember{}  box)
          {}\mRightarrow{}  (\mneg{}(dimension(f1)  =  dimension(f2)))
          {}\mRightarrow{}  ((dimension(f2):=direction(f2))(cube(f1))  =  (dimension(f1):=direction(f1))(cube(f2))))
8.  \mneg{}(x  \mmember{}  J)
9.  l\_subset(Cname;J;I)
10.  \mforall{}y:nameset(J).  \mforall{}c:\mBbbN{}2.    (\mexists{}f\mmember{}box.  face-name(f)  =  <y,  c>)
11.  (\mexists{}f\mmember{}box.  face-name(f)  =  <x,  i>)
12.  (\mforall{}f\mmember{}box.\mneg{}(face-name(f)  =  <x,  1  -  i>))
13.  (\mforall{}f\mmember{}box.(fst(f)  \mmember{}  [x  /  J]))
14.  (\mforall{}f1,f2\mmember{}box.    \mneg{}(face-name(f1)  =  face-name(f2)))
15.  L  :  name-morph(I;[])
16.  ((L  x)  =  i)  \mvee{}  (\mneg{}\muparrow{}null(J))
17.  f  :  I-face(cubical-nerve(C);I)
18.  direction(f)  =  (L  dimension(f))
19.  (f  \mmember{}  box)
20.  v  :  I-face(cubical-nerve(C);I)
21.  (v  \mmember{}  box)
22.  direction(v)  =  (L  dimension(v))
23.  nerve-box-face(box;L)  =  v
24.  \mneg{}(dimension(v)  =  dimension(f))
25.  (dimension(f):=direction(f))(cube(v))  =  (dimension(v):=direction(v))(cube(f))
\mvdash{}  (ob(cube(f))  L)  =  (ob(cube(v))  L)


By

---

Latex:
(MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}cube(v)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (RWO  "cubical-nerve-I-cube"  (-2)  THENA  Auto)
  THEN  Thin  (-1)
  THEN  RenameVar  `F'  (-1)
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}cube(f)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (RWO  "cubical-nerve-I-cube"  (-2)  THENA  Auto)
  THEN  Thin  (-1)
  THEN  RenameVar  `G'  (-1)
  THEN  MoveToConcl  (-1))

---

Home Index