---

Step * 1 of Lemma fl-all-hom_wf


1. I : fset(ℕ)
2. i : {i:ℕ| ¬i ∈ I} 
3. fl-all-hom(I;i) = fl-all-hom(I;i) ∈ Hom(face_lattice(I+i);face_lattice(I))
4. ∀j:names(I)
     ((¬(j = i ∈ ℤ))
     ⇒ (((fl-all-hom(I;i) (j=0)) = (j=0) ∈ Point(face_lattice(I)))
        ∧ ((fl-all-hom(I;i) (j=1)) = (j=1) ∈ Point(face_lattice(I)))))
5. (fl-all-hom(I;i) (i=0)) = 0 ∈ Point(face_lattice(I))
6. (fl-all-hom(I;i) (i=1)) = 0 ∈ Point(face_lattice(I))
7. x : Point(face_lattice(I))
⊢ (fl-all-hom(I;i) x) = x ∈ Point(face_lattice(I))
BY
{ (InstLemma `face-lattice-hom-is-id` [⌜I⌝;⌜fl-all-hom(I;i)⌝]⋅
   THEN Auto
   THEN Try (((DVar `i' THEN DVar `x1') THEN BackThruSomeHyp THEN ParallelOp 3 THEN Complete (Auto)))) }

1
1. I : fset(ℕ)
2. i : {i:ℕ| ¬i ∈ I} 
3. fl-all-hom(I;i) = fl-all-hom(I;i) ∈ Hom(face_lattice(I+i);face_lattice(I))
4. ∀j:names(I)
     ((¬(j = i ∈ ℤ))
     ⇒ (((fl-all-hom(I;i) (j=0)) = (j=0) ∈ Point(face_lattice(I)))
        ∧ ((fl-all-hom(I;i) (j=1)) = (j=1) ∈ Point(face_lattice(I)))))
5. (fl-all-hom(I;i) (i=0)) = 0 ∈ Point(face_lattice(I))
6. (fl-all-hom(I;i) (i=1)) = 0 ∈ Point(face_lattice(I))
7. x : Point(face_lattice(I))
8. fl-all-hom(I;i) = (λx.x) ∈ Hom(face_lattice(I);face_lattice(I))
⊢ (fl-all-hom(I;i) x) = x ∈ Point(face_lattice(I))

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  i  :  \{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
3.  fl-all-hom(I;i)  =  fl-all-hom(I;i)
4.  \mforall{}j:names(I)
          ((\mneg{}(j  =  i))  {}\mRightarrow{}  (((fl-all-hom(I;i)  (j=0))  =  (j=0))  \mwedge{}  ((fl-all-hom(I;i)  (j=1))  =  (j=1))))
5.  (fl-all-hom(I;i)  (i=0))  =  0
6.  (fl-all-hom(I;i)  (i=1))  =  0
7.  x  :  Point(face\_lattice(I))
\mvdash{}  (fl-all-hom(I;i)  x)  =  x


By

---

Latex:
(InstLemma  `face-lattice-hom-is-id`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}fl-all-hom(I;i)\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Try  (((DVar  `i'  THEN  DVar  `x1')  THEN  BackThruSomeHyp  THEN  ParallelOp  3  THEN  Complete  (Auto))))

---

Home Index