---

Step * of Lemma composition-structure-subset

No Annotations
∀[Y,X:j⊢].  ∀[B:{X ⊢ _}]. (X ⊢ Compositon(B) ⊆r Y ⊢ Compositon(B)) supposing sub_cubical_set{j:l}(Y; X)
BY
{ (Intros THEN (D 0 THENA Auto) THEN D -1 THEN (MemTypeCD THENW Auto)) }

1
1. Y : CubicalSet{j}
2. X : CubicalSet{j}
3. sub_cubical_set{j:l}(Y; X)
4. B : {X ⊢ _}
5. x : composition-function{j:l,i:l}(X;B)
6. uniform-comp-function{j:l, i:l}(X; B; x)
⊢ x ∈ composition-function{j:l,i:l}(Y;B)

2
.....set predicate..... 
1. Y : CubicalSet{j}
2. X : CubicalSet{j}
3. sub_cubical_set{j:l}(Y; X)
4. B : {X ⊢ _}
5. x : composition-function{j:l,i:l}(X;B)
6. uniform-comp-function{j:l, i:l}(X; B; x)
⊢ uniform-comp-function{j:l, i:l}(Y; B; x)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Y,X:j\mvdash{}].
    \mforall{}[B:\{X  \mvdash{}  \_\}].  (X  \mvdash{}  Compositon(B)  \msubseteq{}r  Y  \mvdash{}  Compositon(B))  supposing  sub\_cubical\_set\{j:l\}(Y;  X)


By

---

Latex:
(Intros  THEN  (D  0  THENA  Auto)  THEN  D  -1  THEN  (MemTypeCD  THENW  Auto))

---

Home Index