---

Step * of Lemma face-compatible_wf

∀[X:CubicalSet]. ∀[I:Cname List]. ∀[f1,f2:I-face(X;I)].  (face-compatible(X;I;f1;f2) ∈ ℙ)
BY
{ ProveWfLemma }

1
1. X : CubicalSet
2. I : Cname List
3. x : nameset(I)
4. f4 : ℕ2
5. f5 : X(I-[x])
6. x1 : nameset(I)
7. f7 : ℕ2
8. f8 : X(I-[x1])
9. ¬(x = x1 ∈ Cname)
⊢ (x1:=f7) ∈ name-morph(I-[x];I-[x; x1])

2
1. X : CubicalSet
2. I : Cname List
3. x : nameset(I)
4. f4 : ℕ2
5. f5 : X(I-[x])
6. x1 : nameset(I)
7. f7 : ℕ2
8. f8 : X(I-[x1])
9. ¬(x = x1 ∈ Cname)
⊢ (x:=f4) ∈ name-morph(I-[x1];I-[x; x1])

---

Latex:

---

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[I:Cname  List].  \mforall{}[f1,f2:I-face(X;I)].    (face-compatible(X;I;f1;f2)  \mmember{}  \mBbbP{})


By

---

Latex:
ProveWfLemma

---

Home Index