---

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

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

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

2
1. k : ℕ
2. n : ℕ
3. K : n-dim-complex
4. j : ℕ
5. ¬(n = 0 ∈ ℤ)
⊢ |∂(K'^(j))| ≡ |∂(K)|

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  CaseNat  0  `n')

---

Home Index