---

Step * of Lemma fl_all-fl1

∀[I:fset(ℕ)]. ∀[i:ℕ]. ∀[x:names(I+i)].  ((∀i.(x=1)) = if (x =z i) then 0 else (x=1) fi  ∈ Point(face_lattice(I)))
BY
{ (Auto
   THEN Unfold `fl_all` 0
   THEN (InstLemma `fl-all-hom_wf1` [⌜I⌝;⌜i⌝]⋅ THENA Auto)
   THEN (MemTypeHD (-1)⋅ THENA Auto)) }

1
1. I : fset(ℕ)
2. i : ℕ
3. x : names(I+i)
4. fl-all-hom(I;i) = fl-all-hom(I;i) ∈ Hom(face_lattice(I+i);face_lattice(I))
5. (∀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))))))
∧ ((fl-all-hom(I;i) (i=0)) = 0 ∈ Point(face_lattice(I)))
∧ ((fl-all-hom(I;i) (i=1)) = 0 ∈ Point(face_lattice(I)))
⊢ (fl-all-hom(I;i) (x=1)) = if (x =z i) then 0 else (x=1) fi  ∈ Point(face_lattice(I))

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[i:\mBbbN{}].  \mforall{}[x:names(I+i)].    ((\mforall{}i.(x=1))  =  if  (x  =\msubz{}  i)  then  0  else  (x=1)  fi  )


By

---

Latex:
(Auto
  THEN  Unfold  `fl\_all`  0
  THEN  (InstLemma  `fl-all-hom\_wf1`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (MemTypeHD  (-1)\mcdot{}  THENA  Auto))

---

Home Index