---

Step * 1 2 1 1 1 1 of Lemma 0-dim-complex-polyhedron


1. k : ℕ
2. K : ℚCube(k) List
3. no_repeats(ℚCube(k);K)
4. (∀c,d∈K.  Compatible(c;d))
5. ∀c:ℚCube(k). ((c ∈ K) ⇒ (dim(c) = 0 ∈ ℤ))
6. a1 : ℚCube(k)
7. (a1 ∈ K)
8. a2 : ℚCube(k)
9. (a2 ∈ K)
10. (λj.(fst((a1 j)))) = (λj.(fst((a2 j)))) ∈ (ℕk ⟶ ℚ)
11. x : ℕk
12. (fst((a1 x))) = (fst((a2 x))) ∈ ℚ
⊢ (a1 x) = (a2 x) ∈ ℚInterval
BY
{ ((Assert dim(a1) = 0 ∈ ℤ BY Auto) THEN (Assert dim(a2) = 0 ∈ ℤ BY Auto)) }

1
1. k : ℕ
2. K : ℚCube(k) List
3. no_repeats(ℚCube(k);K)
4. (∀c,d∈K.  Compatible(c;d))
5. ∀c:ℚCube(k). ((c ∈ K) ⇒ (dim(c) = 0 ∈ ℤ))
6. a1 : ℚCube(k)
7. (a1 ∈ K)
8. a2 : ℚCube(k)
9. (a2 ∈ K)
10. (λj.(fst((a1 j)))) = (λj.(fst((a2 j)))) ∈ (ℕk ⟶ ℚ)
11. x : ℕk
12. (fst((a1 x))) = (fst((a2 x))) ∈ ℚ
13. dim(a1) = 0 ∈ ℤ
14. dim(a2) = 0 ∈ ℤ
⊢ (a1 x) = (a2 x) ∈ ℚInterval

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  K  :  \mBbbQ{}Cube(k)  List
3.  no\_repeats(\mBbbQ{}Cube(k);K)
4.  (\mforall{}c,d\mmember{}K.    Compatible(c;d))
5.  \mforall{}c:\mBbbQ{}Cube(k).  ((c  \mmember{}  K)  {}\mRightarrow{}  (dim(c)  =  0))
6.  a1  :  \mBbbQ{}Cube(k)
7.  (a1  \mmember{}  K)
8.  a2  :  \mBbbQ{}Cube(k)
9.  (a2  \mmember{}  K)
10.  (\mlambda{}j.(fst((a1  j))))  =  (\mlambda{}j.(fst((a2  j))))
11.  x  :  \mBbbN{}k
12.  (fst((a1  x)))  =  (fst((a2  x)))
\mvdash{}  (a1  x)  =  (a2  x)


By

---

Latex:
((Assert  dim(a1)  =  0  BY  Auto)  THEN  (Assert  dim(a2)  =  0  BY  Auto))

---

Home Index