---

Step * 1 2 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∈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
⊢ (a1 x) = (a2 x) ∈ ℚInterval
BY
{ ((ApFunToHypEquands `Z' ⌜Z x⌝ ⌜ℚ⌝ (-2)⋅ THENA Auto) THEN Reduce -1 THEN (RWO "l_all_iff" 5 THENA 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))) ∈ ℚ
⊢ (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\mmember{}K.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
\mvdash{}  (a1  x)  =  (a2  x)


By

---

Latex:
((ApFunToHypEquands  `Z'  \mkleeneopen{}Z  x\mkleeneclose{}  \mkleeneopen{}\mBbbQ{}\mkleeneclose{}  (-2)\mcdot{}  THENA  Auto)
  THEN  Reduce  -1
  THEN  (RWO  "l\_all\_iff"  5  THENA  Auto))

---

Home Index