---

Step * 1 of Lemma face-term-0-and-1


1. G : CubicalSet{j}
2. I : fset(ℕ)
3. rho : G.𝕀(I)
4. ((q=0) ∧ (q=1))(rho) = 1 ∈ Point(face_lattice(I))
⊢ 0(𝔽)(rho) = 1 ∈ Point(face_lattice(I))
BY
{ (((RWO "face-and-eq-1" (-1) THENA Auto) THEN D -1)
   THEN (FLemma `face-zero-eq-1` [-2] THENA Auto)
   THEN (FLemma `face-one-eq-1` [-2] THENA Auto)
   THEN (Assert ⌜0 = 1 ∈ 𝕀(rho)⌝⋅ THENA Eq)
   THEN (RWO  "interval-type-at" (-1) THENA Auto)
   THEN RepUR ``interval-presheaf`` -1
   THEN Assert ⌜¬(0 = 1 ∈ Point(dM(I)))⌝⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  G  :  CubicalSet\{j\}
2.  I  :  fset(\mBbbN{})
3.  rho  :  G.\mBbbI{}(I)
4.  ((q=0)  \mwedge{}  (q=1))(rho)  =  1
\mvdash{}  0(\mBbbF{})(rho)  =  1


By

---

Latex:
(((RWO  "face-and-eq-1"  (-1)  THENA  Auto)  THEN  D  -1)
  THEN  (FLemma  `face-zero-eq-1`  [-2]  THENA  Auto)
  THEN  (FLemma  `face-one-eq-1`  [-2]  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}0  =  1\mkleeneclose{}\mcdot{}  THENA  Eq)
  THEN  (RWO    "interval-type-at"  (-1)  THENA  Auto)
  THEN  RepUR  ``interval-presheaf``  -1
  THEN  Assert  \mkleeneopen{}\mneg{}(0  =  1)\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index