---

Step * of Lemma face-presheaf-restriction-1

∀[A,B:fset(ℕ)]. ∀[g:B ⟶ A].  (g(1) = 1 ∈ Point(face_lattice(B)))
BY
{ Auto }

1
1. A : fset(ℕ)
2. B : fset(ℕ)
3. g : B ⟶ A
⊢ g(1) = 1 ∈ Point(face_lattice(B))

---

Latex:

---

Latex:
\mforall{}[A,B:fset(\mBbbN{})].  \mforall{}[g:B  {}\mrightarrow{}  A].    (g(1)  =  1)


By

---

Latex:
Auto

---

Home Index