---

Step * 1 of Lemma context-subset_wf


1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. I : fset(ℕ)
4. rho : Gamma(I)
⊢ phi(rho) = 1 ∈ Point(face_lattice(I)) ∈ 𝕌{j'}
BY
{ (InstLemma `face_lattice-point_wf` [⌜parm{j}⌝;⌜I⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  phi  :  \{Gamma  \mvdash{}  \_:\mBbbF{}\}
3.  I  :  fset(\mBbbN{})
4.  rho  :  Gamma(I)
\mvdash{}  phi(rho)  =  1  \mmember{}  \mBbbU{}\{j'\}


By

---

Latex:
(InstLemma  `face\_lattice-point\_wf`  [\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}I\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index