---

Step * of Lemma rat-complex-iter-subdiv-polyhedron

∀[k,n:ℕ]. ∀[K:n-dim-complex]. ∀[j:ℕ].  |K'^(j)| ≡ |K|
BY
{ (Auto THEN NatInd (-1)) }

1
.....basecase..... 
1. k : ℕ
2. n : ℕ
3. K : n-dim-complex
4. j : ℤ
⊢ |K'^(0)| ≡ |K|

2
.....upcase..... 
1. k : ℕ
2. n : ℕ
3. K : n-dim-complex
4. j : ℤ
5. 0 < j
6. |K'^(j - 1)| ≡ |K|
⊢ |K'^(j)| ≡ |K|

---

Latex:

---

Latex:
\mforall{}[k,n:\mBbbN{}].  \mforall{}[K:n-dim-complex].  \mforall{}[j:\mBbbN{}].    |K'\^{}(j)|  \mequiv{}  |K|


By

---

Latex:
(Auto  THEN  NatInd  (-1))

---

Home Index