Step
*
1
1
of Lemma
adjacent-compatible-iff
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. i : ℕ
8. i < ||L||
9. f1 = L[i] ∈ I-face(X;I)
10. i1 : ℕ
11. i1 < ||L||
12. f2 = L[i1] ∈ I-face(X;I)
13. ¬(dimension(f1) = dimension(f2) ∈ Cname)
⊢ (dimension(f2):=direction(f2))(cube(f1))
= (dimension(f1):=direction(f1))(cube(f2))
∈ X(I-[dimension(f1); dimension(f2)])
BY
{ (Decide ⌜i < i1⌝⋅ THENA 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. i : ℕ
8. i < ||L||
9. f1 = L[i] ∈ I-face(X;I)
10. i1 : ℕ
11. i1 < ||L||
12. f2 = L[i1] ∈ I-face(X;I)
13. ¬(dimension(f1) = dimension(f2) ∈ Cname)
14. i < i1
⊢ (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. adjacent-compatible(X;I;L)
5. f1 : I-face(X;I)
6. f2 : I-face(X;I)
7. i : ℕ
8. i < ||L||
9. f1 = L[i] ∈ I-face(X;I)
10. i1 : ℕ
11. i1 < ||L||
12. f2 = L[i1] ∈ I-face(X;I)
13. ¬(dimension(f1) = dimension(f2) ∈ Cname)
14. ¬i < i1
⊢ (dimension(f2):=direction(f2))(cube(f1))
= (dimension(f1):=direction(f1))(cube(f2))
∈ X(I-[dimension(f1); dimension(f2)])
Latex:
Latex:
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. i : \mBbbN{}
8. i < ||L||
9. f1 = L[i]
10. i1 : \mBbbN{}
11. i1 < ||L||
12. f2 = L[i1]
13. \mneg{}(dimension(f1) = dimension(f2))
\mvdash{} (dimension(f2):=direction(f2))(cube(f1)) = (dimension(f1):=direction(f1))(cube(f2))
By
Latex:
(Decide \mkleeneopen{}i < i1\mkleeneclose{}\mcdot{} THENA Auto)
Home
Index