---

Step * of Lemma extend-face-term-morph

∀[I:fset(ℕ)]. ∀[phi:Point(face_lattice(I))]. ∀[u:{I,phi ⊢ _:𝔽}]. ∀[J:fset(ℕ)]. ∀[f:J ⟶ I].
  ((extend-face-term(I;phi;u))<f> = extend-face-term(J;(phi)<f>;(u)subset-trans(I;J;f;phi)) ∈ Point(face_lattice(J)))
BY
{ (Intros THEN BLemma `extend-face-term-unique` THEN Auto) }

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

2
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))

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[phi:Point(face\_lattice(I))].  \mforall{}[u:\{I,phi  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[J:fset(\mBbbN{})].  \mforall{}[f:J  {}\mrightarrow{}  I].
    ((extend-face-term(I;phi;u))<f>  =  extend-face-term(J;(phi)<f>(u)subset-trans(I;J;f;phi)))


By

---

Latex:
(Intros  THEN  BLemma  `extend-face-term-unique`  THEN  Auto)

---

Home Index