---

Step * 1 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
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
BY
{ (BHyp -1 THEN Auto) }

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))
8. K : fset(ℕ)
9. x : J,(phi)<f>(K)
⊢ (<rho> o iota o subset-trans(I;J;f;phi) K x) = (<f(rho)> o iota K x) ∈ Gamma(K)

---

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
7.  \mforall{}[A,B:j\mvdash{}].  \mforall{}[f,g:A  j{}\mrightarrow{}  B].    f  =  g  supposing  \mforall{}K:fset(\mBbbN{}).  \mforall{}x:A(K).    ((f  K  x)  =  (g  K  x))
\mvdash{}  <rho>  o  iota  o  subset-trans(I;J;f;phi)  =  <f(rho)>  o  iota


By

---

Latex:
(BHyp  -1  THEN  Auto)

---

Home Index