---

Step * 1 1 of Lemma rat-sub-div-diameter


1. k : ℕ
2. n : ℕ
3. K : n-dim-complex
4. 0 < ||K||
5. 0 < ||(K)'||
6. v : ℚCube(k) List
7. [%6] : no_repeats(ℚCube(k);v) ∧ (∀c,d∈v.  Compatible(c;d)) ∧ (∀c∈v.dim(c) = n ∈ ℤ)
8. (K)' = v ∈ n-dim-complex
⊢ 0 ≤ (||v|| - 1)
BY
{ (RWO "-1<" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  n  :  \mBbbN{}
3.  K  :  n-dim-complex
4.  0  <  ||K||
5.  0  <  ||(K)'||
6.  v  :  \mBbbQ{}Cube(k)  List
7.  [\%6]  :  no\_repeats(\mBbbQ{}Cube(k);v)  \mwedge{}  (\mforall{}c,d\mmember{}v.    Compatible(c;d))  \mwedge{}  (\mforall{}c\mmember{}v.dim(c)  =  n)
8.  (K)'  =  v
\mvdash{}  0  \mleq{}  (||v||  -  1)


By

---

Latex:
(RWO  "-1<"  0  THEN  Auto)

---

Home Index