---

Step * of Lemma subset-trans-iota-lemma

No Annotations
∀Gamma:j⊢. ∀I:fset(ℕ). ∀rho:Gamma(I). ∀phi:𝔽(I). ∀J:fset(ℕ). ∀f:J ⟶ I.
  (<rho> o iota o subset-trans(I;J;f;phi) = <f(rho)> o iota ∈ J,(phi)<f> j⟶ Gamma)
BY
{ Auto }

1
1. Gamma : CubicalSet{j}
2. I : fset(ℕ)
3. rho : Gamma(I)
4. phi : 𝔽(I)
5. J : fset(ℕ)
6. f : J ⟶ I
⊢ <rho> o iota o subset-trans(I;J;f;phi) = <f(rho)> o iota ∈ J,(phi)<f> j⟶ Gamma

---

Latex:

---

Latex:
No  Annotations
\mforall{}Gamma:j\mvdash{}.  \mforall{}I:fset(\mBbbN{}).  \mforall{}rho:Gamma(I).  \mforall{}phi:\mBbbF{}(I).  \mforall{}J:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I.
    (<rho>  o  iota  o  subset-trans(I;J;f;phi)  =  <f(rho)>  o  iota)


By

---

Latex:
Auto

---

Home Index