---

Step * of Lemma get_face_image

∀[X:CubicalSet]. ∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2]. ∀[bx:open_box(X;I;J;x;i)].
∀[K:Cname List]. ∀[f:name-morph(I;K)]. ∀[c:ℕ2]. ∀[y:nameset(J)].
  get_face(f y;c;open_box_image(X;I;K;f;bx)) = face-image(X;I;K;f;get_face(y;c;bx)) ∈ I-face(X;K) 
  supposing nameset([x / J]) ⊆r name-morph-domain(f;I)
BY
{ (Auto
   THEN RepUR ``get_face`` 0
   THEN (InstLemma `non-trivial-open-box` [⌜X⌝;⌜I⌝;⌜J⌝;⌜x⌝;⌜i⌝;⌜bx⌝;⌜y⌝;⌜c⌝]⋅ THENA Auto)
   THEN Fold `face-direction` 0
   THEN Fold `face-dimension` 0) }

1
1. X : CubicalSet
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. bx : open_box(X;I;J;x;i)
7. K : Cname List
8. f : name-morph(I;K)
9. c : ℕ2
10. y : nameset(J)
11. nameset([x / J]) ⊆r name-morph-domain(f;I)
12. ¬(filter(λf.((dimension(f) =z y) ∧b (direction(f) =z c));bx)
= []
∈ ({f:{f:I-face(X;I)| (f ∈ bx)} | ↑((dimension(f) =z y) ∧b (direction(f) =z c))}  List))
⊢ hd(filter(λf@0.((dimension(f@0) =z f y) ∧b (direction(f@0) =z c));open_box_image(X;I;K;f;bx)))
= face-image(X;I;K;f;hd(filter(λf.((dimension(f) =z y) ∧b (direction(f) =z c));bx)))
∈ I-face(X;K)

---

Latex:

---

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[I:Cname  List].  \mforall{}[J:nameset(I)  List].  \mforall{}[x:nameset(I)].  \mforall{}[i:\mBbbN{}2].
\mforall{}[bx:open\_box(X;I;J;x;i)].  \mforall{}[K:Cname  List].  \mforall{}[f:name-morph(I;K)].  \mforall{}[c:\mBbbN{}2].  \mforall{}[y:nameset(J)].
    get\_face(f  y;c;open\_box\_image(X;I;K;f;bx))  =  face-image(X;I;K;f;get\_face(y;c;bx)) 
    supposing  nameset([x  /  J])  \msubseteq{}r  name-morph-domain(f;I)


By

---

Latex:
(Auto
  THEN  RepUR  ``get\_face``  0
  THEN  (InstLemma  `non-trivial-open-box`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}J\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}bx\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Fold  `face-direction`  0
  THEN  Fold  `face-dimension`  0)

---

Home Index