---

Step * of Lemma cubical-interval-non-trivial-box

∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].
  ∀bx:open_box(cubical-interval();I;J;x;i). ∀h:name-morph(I;[]).
    ((¬(J = [] ∈ (nameset(I) List)))
    ⇒ (¬(filter(λf.(h (fst(f)) =z fst(snd(f)));bx)
       = []
       ∈ ({x:{f:I-face(cubical-interval();I)| (f ∈ bx)} | ↑(h (fst(x)) =z fst(snd(x)))}  List))))
BY
{ Auto }

1
1. I : Cname List
2. J : nameset(I) List
3. x : nameset(I)
4. i : ℕ2
5. bx : open_box(cubical-interval();I;J;x;i)
6. h : name-morph(I;[])
7. ¬(J = [] ∈ (nameset(I) List))
⊢ ¬(filter(λf.(h (fst(f)) =z fst(snd(f)));bx)
= []
∈ ({x:{f:I-face(cubical-interval();I)| (f ∈ bx)} | ↑(h (fst(x)) =z fst(snd(x)))}  List))

---

Latex:

---

Latex:
\mforall{}[I:Cname  List].  \mforall{}[J:nameset(I)  List].  \mforall{}[x:nameset(I)].  \mforall{}[i:\mBbbN{}2].
    \mforall{}bx:open\_box(cubical-interval();I;J;x;i).  \mforall{}h:name-morph(I;[]).
        ((\mneg{}(J  =  []))  {}\mRightarrow{}  (\mneg{}(filter(\mlambda{}f.(h  (fst(f))  =\msubz{}  fst(snd(f)));bx)  =  [])))


By

---

Latex:
Auto

---

Home Index