---

Step * 1 of Lemma face-presheaf-restriction-1


1. A : fset(ℕ)
2. B : fset(ℕ)
3. g : B ⟶ A
⊢ g(1) = 1 ∈ Point(face_lattice(B))
BY
{ (RepUR ``face-presheaf`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  fset(\mBbbN{})
2.  B  :  fset(\mBbbN{})
3.  g  :  B  {}\mrightarrow{}  A
\mvdash{}  g(1)  =  1


By

---

Latex:
(RepUR  ``face-presheaf``  0  THEN  Auto)

---

Home Index