---

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


1. k : ℕ
2. K : ℚCube(k) List
3. no_repeats(ℚCube(k);K) ∧ (∀c,d∈K.  Compatible(c;d)) ∧ (∀c∈K.dim(c) = 0 ∈ ℤ)
⊢ no_repeats(ℕk ⟶ ℚ;map(λp,j. (fst((p j)));K))
BY
{ ((BLemma `no_repeats_map`  THEN Auto)
   THEN D 0
   THEN Reduce 0
   THEN Auto
   THEN DSetVars
   THEN EqTypeCD
   THEN Auto
   THEN Unfold `rational-cube` 0
   THEN (FunExt 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∈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

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  K  :  \mBbbQ{}Cube(k)  List
3.  no\_repeats(\mBbbQ{}Cube(k);K)  \mwedge{}  (\mforall{}c,d\mmember{}K.    Compatible(c;d))  \mwedge{}  (\mforall{}c\mmember{}K.dim(c)  =  0)
\mvdash{}  no\_repeats(\mBbbN{}k  {}\mrightarrow{}  \mBbbQ{};map(\mlambda{}p,j.  (fst((p  j)));K))


By

---

Latex:
((BLemma  `no\_repeats\_map`    THEN  Auto)
  THEN  D  0
  THEN  Reduce  0
  THEN  Auto
  THEN  DSetVars
  THEN  EqTypeCD
  THEN  Auto
  THEN  Unfold  `rational-cube`  0
  THEN  (FunExt  THENA  Auto))

---

Home Index