---

Step * 1 1 of Lemma csm-canonical-section-face-type


1. I : fset(ℕ)
2. K : fset(ℕ)
3. f : K ⟶ I
4. phi : Point(face_lattice(I))
5. J : fset(ℕ)
6. g : J ⟶ K
⊢ ((phi)<f>)<g> = (phi)<f ⋅ g> ∈ 𝔽(g)
BY
{ ((RWO "face-type-at" 0 THENA Auto) THEN (RWO "fl-morph-comp2" 0⋅ THENA Auto) THEN RepeatFor 2 ((EqCD THEN Auto))) }

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  K  :  fset(\mBbbN{})
3.  f  :  K  {}\mrightarrow{}  I
4.  phi  :  Point(face\_lattice(I))
5.  J  :  fset(\mBbbN{})
6.  g  :  J  {}\mrightarrow{}  K
\mvdash{}  ((phi)<f>)<g>  =  (phi)<f  \mcdot{}  g>


By

---

Latex:
((RWO  "face-type-at"  0  THENA  Auto)
  THEN  (RWO  "fl-morph-comp2"  0\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  ((EqCD  THEN  Auto)))

---

Home Index