---

Step * 1 of Lemma fl-join_wf


1. I : fset(ℕ)
2. x : 𝔽(I)
3. y : 𝔽(I)
⊢ fl-join(I;x;y) ∈ 𝔽(I)
BY
{ All (RepUR ``I_cube face-presheaf functor-ob``) }

1
1. I : fset(ℕ)
2. x : Point(face_lattice(I))
3. y : Point(face_lattice(I))
⊢ fl-join(I;x;y) ∈ Point(face_lattice(I))

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  x  :  \mBbbF{}(I)
3.  y  :  \mBbbF{}(I)
\mvdash{}  fl-join(I;x;y)  \mmember{}  \mBbbF{}(I)


By

---

Latex:
All  (RepUR  ``I\_cube  face-presheaf  functor-ob``)

---

Home Index