---

Step * 1 1 1 of Lemma CCC-finite


1. n : ℕ
2. k : ℕ
3. n ≤ 2^k
4. ∀m:ℕ3. CCC(ℕm)
⊢ CCC(ℕn)
BY
{ ((Decide ⌜n ≤ 2⌝⋅ THENA Auto) THENL [BackThruSomeHyp; (InstLemma `CCC-surjection` [⌜ℕ2^k⌝;⌜ℕn⌝]⋅ THEN Auto)]) }

1
.....antecedent..... 
1. n : ℕ
2. k : ℕ
3. n ≤ 2^k
4. ∀m:ℕ3. CCC(ℕm)
5. ¬(n ≤ 2)
⊢ ∃f:ℕ2^k ⟶ ℕn. Surj(ℕ2^k;ℕn;f)

2
.....antecedent..... 
1. n : ℕ
2. k : ℕ
3. n ≤ 2^k
4. ∀m:ℕ3. CCC(ℕm)
5. ¬(n ≤ 2)
⊢ CCC(ℕ2^k)

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  k  :  \mBbbN{}
3.  n  \mleq{}  2\^{}k
4.  \mforall{}m:\mBbbN{}3.  CCC(\mBbbN{}m)
\mvdash{}  CCC(\mBbbN{}n)


By

---

Latex:
((Decide  \mkleeneopen{}n  \mleq{}  2\mkleeneclose{}\mcdot{}  THENA  Auto)
  THENL  [BackThruSomeHyp;  (InstLemma  `CCC-surjection`  [\mkleeneopen{}\mBbbN{}2\^{}k\mkleeneclose{};\mkleeneopen{}\mBbbN{}n\mkleeneclose{}]\mcdot{}  THEN  Auto)]
)

---

Home Index