---

Step * 1 1 of Lemma empty-context-subset-lemma5


1. Gamma : CubicalSet{j}
2. i : {Gamma ⊢ _:𝕀}
3. I : fset(ℕ)
4. Gamma, (i=0), (i=1)(I)
⊢ False
BY
{ (RepUR ``context-subset`` -1
   THEN D -1
   THEN D -2
   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.  Gamma  :  CubicalSet\{j\}
2.  i  :  \{Gamma  \mvdash{}  \_:\mBbbI{}\}
3.  I  :  fset(\mBbbN{})
4.  Gamma,  (i=0),  (i=1)(I)
\mvdash{}  False


By

---

Latex:
(RepUR  ``context-subset``  -1
  THEN  D  -1
  THEN  D  -2
  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