---

Step * 1 of Lemma subset-trans-iota-lemma


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
BY
{ InstLemma `csm-equal2` [⌜parm{j}⌝]⋅ }

1
1. Gamma : CubicalSet{j}
2. I : fset(ℕ)
3. rho : Gamma(I)
4. phi : 𝔽(I)
5. J : fset(ℕ)
6. f : J ⟶ I
7. ∀[A,B:j⊢]. ∀[f,g:A j⟶ B].  f = g ∈ A j⟶ B supposing ∀K:fset(ℕ). ∀x:A(K).  ((f K x) = (g K x) ∈ B(K))
⊢ <rho> o iota o subset-trans(I;J;f;phi) = <f(rho)> o iota ∈ J,(phi)<f> j⟶ Gamma

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  I  :  fset(\mBbbN{})
3.  rho  :  Gamma(I)
4.  phi  :  \mBbbF{}(I)
5.  J  :  fset(\mBbbN{})
6.  f  :  J  {}\mrightarrow{}  I
\mvdash{}  <rho>  o  iota  o  subset-trans(I;J;f;phi)  =  <f(rho)>  o  iota


By

---

Latex:
InstLemma  `csm-equal2`  [\mkleeneopen{}parm\{j\}\mkleeneclose{}]\mcdot{}

---

Home Index