---

Step * of Lemma rat-complex-boundary-boundary

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

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

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

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  CaseNat  0  `n')

---

Home Index