---

Step * 1 of Lemma case-cube_wf


1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. A : {Gamma, phi ⊢ _}
5. B : {Gamma, psi ⊢ _}
6. I : fset(ℕ)
7. rho : Gamma(I)
8. (phi(rho) = 1 ∈ Point(face_lattice(I))) ∨ (psi(rho) = 1 ∈ Point(face_lattice(I)))
⊢ case-cube(phi;A;B;I;rho) ∈ Type
BY
{ ProveWfLemma }

1
.....set predicate..... 
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. A : {Gamma, phi ⊢ _}
5. B : {Gamma, psi ⊢ _}
6. I : fset(ℕ)
7. rho : Gamma(I)
8. (phi(rho) = 1 ∈ Point(face_lattice(I))) ∨ (psi(rho) = 1 ∈ Point(face_lattice(I)))
9. ¬(phi(rho) = 1 ∈ Point(face_lattice(I)))
⊢ psi(rho) = 1 ∈ Point(face_lattice(I))

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  phi  :  \{Gamma  \mvdash{}  \_:\mBbbF{}\}
3.  psi  :  \{Gamma  \mvdash{}  \_:\mBbbF{}\}
4.  A  :  \{Gamma,  phi  \mvdash{}  \_\}
5.  B  :  \{Gamma,  psi  \mvdash{}  \_\}
6.  I  :  fset(\mBbbN{})
7.  rho  :  Gamma(I)
8.  (phi(rho)  =  1)  \mvee{}  (psi(rho)  =  1)
\mvdash{}  case-cube(phi;A;B;I;rho)  \mmember{}  Type


By

---

Latex:
ProveWfLemma

---

Home Index