---

Step * of Lemma empty-cubical-subset-I_cube

∀[I,J:fset(ℕ)].  (¬I,0(J))
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN RepUR ``cubical-subset I_cube functor-ob rep-sub-sheaf cat-arrow cube-cat`` -1
   THEN D -1
   THEN RepUR ``name-morph-satisfies`` -1
   THEN (RWO "fl-morph-0" (-1) THENA Auto)) }

1
1. I : fset(ℕ)
2. J : fset(ℕ)
3. f : J ⟶ I
4. 0 = 1 ∈ Point(face_lattice(J))
⊢ False

---

Latex:

---

Latex:
\mforall{}[I,J:fset(\mBbbN{})].    (\mneg{}I,0(J))


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  RepUR  ``cubical-subset  I\_cube  functor-ob  rep-sub-sheaf  cat-arrow  cube-cat``  -1
  THEN  D  -1
  THEN  RepUR  ``name-morph-satisfies``  -1
  THEN  (RWO  "fl-morph-0"  (-1)  THENA  Auto))

---

Home Index