---

Step * of Lemma boundary-polyhedron-subtype

∀[k:ℕ]. ∀[n:ℕ+]. ∀[K:n-dim-complex].  (|∂(K)| ⊆r |K|)
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN D -1
   THEN MemTypeCD
   THEN Auto
   THEN ((SupposeMore (-1) THENM RemoveDoubleNegation)
         THENA (Try (QuickAuto) THEN Try (((GenConclTerm ⌜∂(K)⌝⋅ THENA Auto) THEN D -2 THEN Auto)))
         )
   THEN D -1) }

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

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[K:n-dim-complex].    (|\mpartial{}(K)|  \msubseteq{}r  |K|)


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  MemTypeCD
  THEN  Auto
  THEN  ((SupposeMore  (-1)  THENM  RemoveDoubleNegation)
              THENA  (Try  (QuickAuto)  THEN  Try  (((GenConclTerm  \mkleeneopen{}\mpartial{}(K)\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  D  -2  THEN  Auto)))
              )
  THEN  D  -1)

---

Home Index