---

Step * 1 2 of Lemma boundary-polyhedron-subtype


1. k : ℕ
2. n : ℕ+
3. K : n-dim-complex
4. x : ℝ^k
5. i : ℕ||∂(K)||
6. in-rat-cube(k;x;∂(K)[i])
7. (∃c:ℚCube(k). ((c ∈ K) ∧ (↑Inhabited(c)) ∧ ∂(K)[i] ≤ c ∧ (dim(∂(K)[i]) = (dim(c) - 1) ∈ ℤ)))
∧ (↑in-complex-boundary(k;∂(K)[i];K))
⊢ ∃i:ℕ||K||. in-rat-cube(k;x;K[i])
BY
{ ((ExRepD THEN D -5) THEN D 0 With ⌜i1⌝  THEN Auto) }

1
1. k : ℕ
2. n : ℕ+
3. K : n-dim-complex
4. x : ℝ^k
5. i : ℕ||∂(K)||
6. in-rat-cube(k;x;∂(K)[i])
7. c : ℚCube(k)
8. i1 : ℕ
9. i1 < ||K|| c∧ (c = K[i1] ∈ ℚCube(k))
10. ↑Inhabited(c)
11. ∂(K)[i] ≤ c
12. dim(∂(K)[i]) = (dim(c) - 1) ∈ ℤ
13. ↑in-complex-boundary(k;∂(K)[i];K)
⊢ in-rat-cube(k;x;K[i1])

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  n  :  \mBbbN{}\msupplus{}
3.  K  :  n-dim-complex
4.  x  :  \mBbbR{}\^{}k
5.  i  :  \mBbbN{}||\mpartial{}(K)||
6.  in-rat-cube(k;x;\mpartial{}(K)[i])
7.  (\mexists{}c:\mBbbQ{}Cube(k).  ((c  \mmember{}  K)  \mwedge{}  (\muparrow{}Inhabited(c))  \mwedge{}  \mpartial{}(K)[i]  \mleq{}  c  \mwedge{}  (dim(\mpartial{}(K)[i])  =  (dim(c)  -  1))))
\mwedge{}  (\muparrow{}in-complex-boundary(k;\mpartial{}(K)[i];K))
\mvdash{}  \mexists{}i:\mBbbN{}||K||.  in-rat-cube(k;x;K[i])


By

---

Latex:
((ExRepD  THEN  D  -5)  THEN  D  0  With  \mkleeneopen{}i1\mkleeneclose{}    THEN  Auto)

---

Home Index