---

Step * of Lemma rat-complex-boundary_wf

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

1
1. k : ℕ
2. n : ℕ
3. K : n-dim-complex
4. n = 0 ∈ ℤ
⊢ ∂(K) ∈ 0 - 1-dim-complex

2
1. k : ℕ
2. n : ℕ
3. K : n-dim-complex
4. ¬(n = 0 ∈ ℤ)
⊢ ∂(K) ∈ n - 1-dim-complex

---

Latex:

---

Latex:
\mforall{}[k,n:\mBbbN{}].  \mforall{}[K:n-dim-complex].    (\mpartial{}(K)  \mmember{}  n  -  1-dim-complex)


By

---

Latex:
(Auto  THEN  CaseNat  0    `n')

---

Home Index