---

Step * of Lemma rat-cube-complex-polyhedron-closed

∀[k:ℕ]. ∀[K:ℚCube(k) List]. ∀[v:|K|]. ∀[x:ℝ^k].  x ∈ |K| supposing v ≡ x
BY
{ (Auto THEN DVar `v' THEN (MemTypeCD THEN Auto) THEN ParallelOp -3 THEN ParallelLast THEN RWO "-2" (-1) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[K:\mBbbQ{}Cube(k)  List].  \mforall{}[v:|K|].  \mforall{}[x:\mBbbR{}\^{}k].    x  \mmember{}  |K|  supposing  v  \mequiv{}  x


By

---

Latex:
(Auto
  THEN  DVar  `v'
  THEN  (MemTypeCD  THEN  Auto)
  THEN  ParallelOp  -3
  THEN  ParallelLast
  THEN  RWO  "-2"  (-1)
  THEN  Auto)

---

Home Index