---

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


1. k : ℕ
2. K : 0-dim-complex
3. x : |K|
⊢ no_repeats(ℕk ⟶ ℚ;[]) ⇒ Stable{∃i:ℕ||[]||. req-vec(k;x;λj.rat2real([][i] j))}
BY
{ (((Reduce 0 THEN Auto) THEN (D 0 THENA Auto)) THEN Assert ⌜False⌝⋅ THEN Auto THEN D -1 THEN Auto) }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  K  :  0-dim-complex
3.  x  :  |K|
\mvdash{}  no\_repeats(\mBbbN{}k  {}\mrightarrow{}  \mBbbQ{};[])  {}\mRightarrow{}  Stable\{\mexists{}i:\mBbbN{}||[]||.  req-vec(k;x;\mlambda{}j.rat2real([][i]  j))\}


By

---

Latex:
(((Reduce  0  THEN  Auto)  THEN  (D  0  THENA  Auto))  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  D  -1  THEN  Auto)

---

Home Index