---

Step * of Lemma adjacent-compatible-iff

∀[X:CubicalSet]
  ∀I:Cname List. ∀L:I-face(X;I) List.
    uiff(adjacent-compatible(X;I;L);∀f1,f2:I-face(X;I).
                                      ((f1 ∈ L)
                                      ⇒ (f2 ∈ L)
                                      ⇒ (¬(dimension(f1) = dimension(f2) ∈ Cname))
                                      ⇒ ((dimension(f2):=direction(f2))(cube(f1))
                                         = (dimension(f1):=direction(f1))(cube(f2))
                                         ∈ X(I-[dimension(f1); dimension(f2)]))))
BY
{ (Auto THEN Try ((FaceMapDiff2 THEN Auto))) }

1
1. X : CubicalSet
2. I : Cname List
3. L : I-face(X;I) List
4. adjacent-compatible(X;I;L)
5. f1 : I-face(X;I)
6. f2 : I-face(X;I)
7. (f1 ∈ L)
8. (f2 ∈ L)
9. ¬(dimension(f1) = dimension(f2) ∈ Cname)
⊢ (dimension(f2):=direction(f2))(cube(f1))
= (dimension(f1):=direction(f1))(cube(f2))
∈ X(I-[dimension(f1); dimension(f2)])

2
1. [X] : CubicalSet
2. I : Cname List
3. L : I-face(X;I) List
4. ∀f1,f2:I-face(X;I).
     ((f1 ∈ L)
     ⇒ (f2 ∈ L)
     ⇒ (¬(dimension(f1) = dimension(f2) ∈ Cname))
     ⇒ ((dimension(f2):=direction(f2))(cube(f1))
        = (dimension(f1):=direction(f1))(cube(f2))
        ∈ X(I-[dimension(f1); dimension(f2)])))
⊢ adjacent-compatible(X;I;L)

---

Latex:

---

Latex:
\mforall{}[X:CubicalSet]
    \mforall{}I:Cname  List.  \mforall{}L:I-face(X;I)  List.
        uiff(adjacent-compatible(X;I;L);\mforall{}f1,f2:I-face(X;I).
                                                                            ((f1  \mmember{}  L)
                                                                            {}\mRightarrow{}  (f2  \mmember{}  L)
                                                                            {}\mRightarrow{}  (\mneg{}(dimension(f1)  =  dimension(f2)))
                                                                            {}\mRightarrow{}  ((dimension(f2):=direction(f2))(cube(f1))
                                                                                  =  (dimension(f1):=direction(f1))(cube(f2)))))


By

---

Latex:
(Auto  THEN  Try  ((FaceMapDiff2  THEN  Auto)))

---

Home Index