---

Step * 1 of Lemma fl-morph-comp-1


1. J : fset(ℕ)
2. K : fset(ℕ)
3. f : K ⟶ J
4. z : Point(dM(J))
5. h : dma-hom(dM(J);dM(K))
6. ∀i:names(J). ((h <i>) = (f i) ∈ Point(dM(K)))
⊢ (dM-to-FL(J;z))<f> = dM-to-FL(K;h z) ∈ Point(face_lattice(K))
BY
{ (InstLemma `dM-hom-unique` [⌜J⌝;⌜face_lattice(K)⌝;⌜face_lattice-deq()⌝]⋅ THENA Auto) }

1
1. J : fset(ℕ)
2. K : fset(ℕ)
3. f : K ⟶ J
4. z : Point(dM(J))
5. h : dma-hom(dM(J);dM(K))
6. ∀i:names(J). ((h <i>) = (f i) ∈ Point(dM(K)))
7. ∀[g,h:Hom(dM(J);face_lattice(K))].
     g = h ∈ Hom(dM(J);face_lattice(K)) 
     supposing ∀i:names(J)
                 (((g <i>) = (h <i>) ∈ Point(face_lattice(K))) ∧ ((g <1-i>) = (h <1-i>) ∈ Point(face_lattice(K))))
⊢ (dM-to-FL(J;z))<f> = dM-to-FL(K;h z) ∈ Point(face_lattice(K))

---

Latex:

---

Latex:

1.  J  :  fset(\mBbbN{})
2.  K  :  fset(\mBbbN{})
3.  f  :  K  {}\mrightarrow{}  J
4.  z  :  Point(dM(J))
5.  h  :  dma-hom(dM(J);dM(K))
6.  \mforall{}i:names(J).  ((h  <i>)  =  (f  i))
\mvdash{}  (dM-to-FL(J;z))<f>  =  dM-to-FL(K;h  z)


By

---

Latex:
(InstLemma  `dM-hom-unique`  [\mkleeneopen{}J\mkleeneclose{};\mkleeneopen{}face\_lattice(K)\mkleeneclose{};\mkleeneopen{}face\_lattice-deq()\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index