---

Step * 2 1 1 1 1 1 1 1 of Lemma poset-functor-extends-box-faces-1


1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. bx : I-face(cubical-nerve(cat(G));I) List
7. adjacent-compatible(cubical-nerve(cat(G));I;bx)
8. ¬(x ∈ J)
9. l_subset(Cname;J;I)
10. ∀y:nameset(J). ∀c:ℕ2.  (∃f∈bx. face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
11. (∃f∈bx. face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
12. (∀f∈bx.¬(face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
13. (∀f∈bx.(fst(f) ∈ [x / J]))
14. (∀f1,f2∈bx.  ¬(face-name(f1) = face-name(f2) ∈ (nameset(I) × ℕ2)))
15. ¬↑null(J)
16. (∀j'∈J.j' = hd(J) ∈ Cname)
17. i1 : ℕ||bx||
18. ∀f:name-morph(I-[dimension(bx[i1])];[]). (((dimension(bx[i1]):=direction(bx[i1])) o f) ∈ name-morph(I;[]))
19. i2 : Cname
20. (i2 ∈ I)
21. ¬(i2 = dimension(bx[i1]) ∈ Cname)
22. c : {c:name-morph(I-[dimension(bx[i1])];[])| (c i2) = 0 ∈ ℕ2} 
23. ((dimension(bx[i1]):=direction(bx[i1])) o c) ∈ name-morph(I;[])
24. (((dimension(bx[i1]):=direction(bx[i1])) o c) i2) = 0 ∈ ℕ2
25. i2 = hd(J) ∈ Cname
⊢ (((dimension(bx[i1]):=direction(bx[i1])) o c) x) = i ∈ ℤ
BY
{ TACTIC:((Assert (dimension(bx[i1]) ∈ [x / J]) BY
                 OnMaybeHyp 13 (\h. ((With ⌜i1⌝ (D h)⋅ THENA Auto) THEN Fold `face-dimension` (-1) THEN Auto)))
          THEN (RW ListC (-1) THENA Auto)
          THEN D -1) }

1
1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. bx : I-face(cubical-nerve(cat(G));I) List
7. adjacent-compatible(cubical-nerve(cat(G));I;bx)
8. ¬(x ∈ J)
9. l_subset(Cname;J;I)
10. ∀y:nameset(J). ∀c:ℕ2.  (∃f∈bx. face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
11. (∃f∈bx. face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
12. (∀f∈bx.¬(face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
13. (∀f∈bx.(fst(f) ∈ [x / J]))
14. (∀f1,f2∈bx.  ¬(face-name(f1) = face-name(f2) ∈ (nameset(I) × ℕ2)))
15. ¬↑null(J)
16. (∀j'∈J.j' = hd(J) ∈ Cname)
17. i1 : ℕ||bx||
18. ∀f:name-morph(I-[dimension(bx[i1])];[]). (((dimension(bx[i1]):=direction(bx[i1])) o f) ∈ name-morph(I;[]))
19. i2 : Cname
20. (i2 ∈ I)
21. ¬(i2 = dimension(bx[i1]) ∈ Cname)
22. c : {c:name-morph(I-[dimension(bx[i1])];[])| (c i2) = 0 ∈ ℕ2} 
23. ((dimension(bx[i1]):=direction(bx[i1])) o c) ∈ name-morph(I;[])
24. (((dimension(bx[i1]):=direction(bx[i1])) o c) i2) = 0 ∈ ℕ2
25. i2 = hd(J) ∈ Cname
26. dimension(bx[i1]) = x ∈ Cname
⊢ (((dimension(bx[i1]):=direction(bx[i1])) o c) x) = i ∈ ℤ

2
1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. bx : I-face(cubical-nerve(cat(G));I) List
7. adjacent-compatible(cubical-nerve(cat(G));I;bx)
8. ¬(x ∈ J)
9. l_subset(Cname;J;I)
10. ∀y:nameset(J). ∀c:ℕ2.  (∃f∈bx. face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
11. (∃f∈bx. face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
12. (∀f∈bx.¬(face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
13. (∀f∈bx.(fst(f) ∈ [x / J]))
14. (∀f1,f2∈bx.  ¬(face-name(f1) = face-name(f2) ∈ (nameset(I) × ℕ2)))
15. ¬↑null(J)
16. (∀j'∈J.j' = hd(J) ∈ Cname)
17. i1 : ℕ||bx||
18. ∀f:name-morph(I-[dimension(bx[i1])];[]). (((dimension(bx[i1]):=direction(bx[i1])) o f) ∈ name-morph(I;[]))
19. i2 : Cname
20. (i2 ∈ I)
21. ¬(i2 = dimension(bx[i1]) ∈ Cname)
22. c : {c:name-morph(I-[dimension(bx[i1])];[])| (c i2) = 0 ∈ ℕ2} 
23. ((dimension(bx[i1]):=direction(bx[i1])) o c) ∈ name-morph(I;[])
24. (((dimension(bx[i1]):=direction(bx[i1])) o c) i2) = 0 ∈ ℕ2
25. i2 = hd(J) ∈ Cname
26. (dimension(bx[i1]) ∈ J)
⊢ (((dimension(bx[i1]):=direction(bx[i1])) o c) x) = i ∈ ℤ

---

Latex:

---

Latex:

1.  G  :  Groupoid
2.  I  :  Cname  List
3.  J  :  nameset(I)  List
4.  x  :  nameset(I)
5.  i  :  \mBbbN{}2
6.  bx  :  I-face(cubical-nerve(cat(G));I)  List
7.  adjacent-compatible(cubical-nerve(cat(G));I;bx)
8.  \mneg{}(x  \mmember{}  J)
9.  l\_subset(Cname;J;I)
10.  \mforall{}y:nameset(J).  \mforall{}c:\mBbbN{}2.    (\mexists{}f\mmember{}bx.  face-name(f)  =  <y,  c>)
11.  (\mexists{}f\mmember{}bx.  face-name(f)  =  <x,  i>)
12.  (\mforall{}f\mmember{}bx.\mneg{}(face-name(f)  =  <x,  1  -  i>))
13.  (\mforall{}f\mmember{}bx.(fst(f)  \mmember{}  [x  /  J]))
14.  (\mforall{}f1,f2\mmember{}bx.    \mneg{}(face-name(f1)  =  face-name(f2)))
15.  \mneg{}\muparrow{}null(J)
16.  (\mforall{}j'\mmember{}J.j'  =  hd(J))
17.  i1  :  \mBbbN{}||bx||
18.  \mforall{}f:name-morph(I-[dimension(bx[i1])];[])
            (((dimension(bx[i1]):=direction(bx[i1]))  o  f)  \mmember{}  name-morph(I;[]))
19.  i2  :  Cname
20.  (i2  \mmember{}  I)
21.  \mneg{}(i2  =  dimension(bx[i1]))
22.  c  :  \{c:name-morph(I-[dimension(bx[i1])];[])|  (c  i2)  =  0\} 
23.  ((dimension(bx[i1]):=direction(bx[i1]))  o  c)  \mmember{}  name-morph(I;[])
24.  (((dimension(bx[i1]):=direction(bx[i1]))  o  c)  i2)  =  0
25.  i2  =  hd(J)
\mvdash{}  (((dimension(bx[i1]):=direction(bx[i1]))  o  c)  x)  =  i


By

---

Latex:
TACTIC:((Assert  (dimension(bx[i1])  \mmember{}  [x  /  J])  BY
                              OnMaybeHyp  13  (\mbackslash{}h.  ((With  \mkleeneopen{}i1\mkleeneclose{}  (D  h)\mcdot{}  THENA  Auto)
                                                                      THEN  Fold  `face-dimension`  (-1)
                                                                      THEN  Auto)))
                THEN  (RW  ListC  (-1)  THENA  Auto)
                THEN  D  -1)

---

Home Index