---

Step * 1 2 1 1 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))) ∈ ℚ
13. (fst((a1 x))) = (snd((a1 x))) ∈ ℚ
14. (fst((a2 x))) = (snd((a2 x))) ∈ ℚ
⊢ (a1 x) = (a2 x) ∈ ℚInterval
BY
{ (RepeatFor 3 (MoveToConcl (-1))
   THEN GenConclTerms Auto [⌜a1 x⌝;⌜a2 x⌝]⋅
   THEN All Thin
   THEN D -2
   THEN D -1
   THEN Reduce 0
   THEN Auto) }

---

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)))
13.  (fst((a1  x)))  =  (snd((a1  x)))
14.  (fst((a2  x)))  =  (snd((a2  x)))
\mvdash{}  (a1  x)  =  (a2  x)


By

---

Latex:
(RepeatFor  3  (MoveToConcl  (-1))
  THEN  GenConclTerms  Auto  [\mkleeneopen{}a1  x\mkleeneclose{};\mkleeneopen{}a2  x\mkleeneclose{}]\mcdot{}
  THEN  All  Thin
  THEN  D  -2
  THEN  D  -1
  THEN  Reduce  0
  THEN  Auto)

---

Home Index