---

Step * 2 of Lemma extend-face-term-morph


1. I : fset(ℕ)
2. phi : Point(face_lattice(I))
3. u : {I,phi ⊢ _:𝔽}
4. J : fset(ℕ)
5. f : J ⟶ I
6. (extend-face-term(I;phi;u))<f> ≤ (phi)<f>
7. g : {f1:J ⟶ J| ((phi)<f> f1) = 1} 
⊢ ((extend-face-term(I;phi;u))<f>)<g> = (u)subset-trans(I;J;f;phi)(g) ∈ Point(face_lattice(J))
BY
{ D -1 }

1
1. I : fset(ℕ)
2. phi : Point(face_lattice(I))
3. u : {I,phi ⊢ _:𝔽}
4. J : fset(ℕ)
5. f : J ⟶ I
6. (extend-face-term(I;phi;u))<f> ≤ (phi)<f>
7. g : J ⟶ J
8. ((phi)<f> g) = 1
⊢ ((extend-face-term(I;phi;u))<f>)<g> = (u)subset-trans(I;J;f;phi)(g) ∈ Point(face_lattice(J))

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  phi  :  Point(face\_lattice(I))
3.  u  :  \{I,phi  \mvdash{}  \_:\mBbbF{}\}
4.  J  :  fset(\mBbbN{})
5.  f  :  J  {}\mrightarrow{}  I
6.  (extend-face-term(I;phi;u))<f>  \mleq{}  (phi)<f>
7.  g  :  \{f1:J  {}\mrightarrow{}  J|  ((phi)<f>  f1)  =  1\} 
\mvdash{}  ((extend-face-term(I;phi;u))<f>)<g>  =  (u)subset-trans(I;J;f;phi)(g)


By

---

Latex:
D  -1

---

Home Index