---

Step * of Lemma length-rat-complex-boundary-even

No Annotations
∀k,n:ℕ. ∀K:n-dim-complex.  (↑isEven(||∂(K)||))
BY
{ (Auto
   THEN (CaseNat 0 `n'
         THENL [(RWO "rat-complex-boundary-0-dim" 0 THEN Auto)
               ; ((Assert ⌜∀m:ℕ. ∀K:n-dim-complex.  (||K|| < m ⇒ (↑isEven(||∂(K)||)))⌝⋅
                  THENM (InstHyp [⌜||K|| + 1⌝;⌜K⌝] (-1)⋅ THEN Auto)
                  )
                  THEN Thin (-2)
                  THEN InductionOnNat
                  THEN Auto
                  THEN (Assert 0 ≤ ||K|| BY
                              Auto)
                  THEN Auto)]
        )
   ) }

1
1. k : ℕ
2. n : ℕ
3. ¬(n = 0 ∈ ℤ)
4. m : ℤ
5. 0 < m
6. ∀K:n-dim-complex. (||K|| < m - 1 ⇒ (↑isEven(||∂(K)||)))
7. K : n-dim-complex
8. ||K|| < m
9. 0 ≤ ||K||
⊢ ↑isEven(||∂(K)||)

---

Latex:

---

Latex:
No  Annotations
\mforall{}k,n:\mBbbN{}.  \mforall{}K:n-dim-complex.    (\muparrow{}isEven(||\mpartial{}(K)||))


By

---

Latex:
(Auto
  THEN  (CaseNat  0  `n'
              THENL  [(RWO  "rat-complex-boundary-0-dim"  0  THEN  Auto)
                          ;  ((Assert  \mkleeneopen{}\mforall{}m:\mBbbN{}.  \mforall{}K:n-dim-complex.    (||K||  <  m  {}\mRightarrow{}  (\muparrow{}isEven(||\mpartial{}(K)||)))\mkleeneclose{}\mcdot{}
                                THENM  (InstHyp  [\mkleeneopen{}||K||  +  1\mkleeneclose{};\mkleeneopen{}K\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)
                                )
                                THEN  Thin  (-2)
                                THEN  InductionOnNat
                                THEN  Auto
                                THEN  (Assert  0  \mleq{}  ||K||  BY
                                                        Auto)
                                THEN  Auto)]
            )
  )

---

Home Index