---

Step * of Lemma get_face_unique

∀X:CubicalSet. ∀I:Cname List. ∀f:I-face(X;I). ∀J:nameset(I) List. ∀x:nameset(I). ∀i:ℕ2. ∀box:open_box(X;I;J;x;i).
  ((f ∈ box) ⇒ (get_face(dimension(f);direction(f);box) = f ∈ I-face(X;I)))
BY
{ (Auto THEN GenConclTerm ⌜get_face(dimension(f);direction(f);box)⌝⋅) }

1
.....wf..... 
1. X : CubicalSet
2. I : Cname List
3. f : I-face(X;I)
4. J : nameset(I) List
5. x : nameset(I)
6. i : ℕ2
7. box : open_box(X;I;J;x;i)
8. (f ∈ box)
⊢ get_face(dimension(f);direction(f);box) ∈ {f1:I-face(X;I)| 
                                             (f1 ∈ box)
                                             ∧ (face-name(f1) = <dimension(f), direction(f)> ∈ (nameset(I) × ℕ2))} 

2
1. X : CubicalSet
2. I : Cname List
3. f : I-face(X;I)
4. J : nameset(I) List
5. x : nameset(I)
6. i : ℕ2
7. box : open_box(X;I;J;x;i)
8. (f ∈ box)
9. v : {f1:I-face(X;I)| (f1 ∈ box) ∧ (face-name(f1) = <dimension(f), direction(f)> ∈ (nameset(I) × ℕ2))} 
10. get_face(dimension(f);direction(f);box)
= v
∈ {f1:I-face(X;I)| (f1 ∈ box) ∧ (face-name(f1) = <dimension(f), direction(f)> ∈ (nameset(I) × ℕ2))} 
⊢ v = f ∈ I-face(X;I)

---

Latex:

---

Latex:
\mforall{}X:CubicalSet.  \mforall{}I:Cname  List.  \mforall{}f:I-face(X;I).  \mforall{}J:nameset(I)  List.  \mforall{}x:nameset(I).  \mforall{}i:\mBbbN{}2.
\mforall{}box:open\_box(X;I;J;x;i).
    ((f  \mmember{}  box)  {}\mRightarrow{}  (get\_face(dimension(f);direction(f);box)  =  f))


By

---

Latex:
(Auto  THEN  GenConclTerm  \mkleeneopen{}get\_face(dimension(f);direction(f);box)\mkleeneclose{}\mcdot{})

---

Home Index