---

Step * 1 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])
⊢ ∃i:ℕ||K||. in-rat-cube(k;x;K[i])
BY
{ ((Assert (∂(K)[i] ∈ ∂(K)) BY Auto) THEN RWO "member-rat-complex-boundary" (-1) THEN Try (QuickAuto)) }

1
.....wf..... 
1. k : ℕ
2. n : ℕ+
3. K : n-dim-complex
4. x : ℝ^k
5. i : ℕ||∂(K)||
6. in-rat-cube(k;x;∂(K)[i])
7. (∂(K)[i] ∈ ∂(K))
⊢ ∂(K)[i] ∈ ℚCube(k)

2
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])

---

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])
\mvdash{}  \mexists{}i:\mBbbN{}||K||.  in-rat-cube(k;x;K[i])


By

---

Latex:
((Assert  (\mpartial{}(K)[i]  \mmember{}  \mpartial{}(K))  BY  Auto)  THEN  RWO  "member-rat-complex-boundary"  (-1)  THEN  Try  (QuickAuto))

---

Home Index