Step
*
1
1
of Lemma
decidable-exists-finite
1. [T] : Type
2. n : ℕ
3. T ~ ℕn
⊢ ∃f:ℕn ⟶ T. Surj(ℕn;T;f)
BY
{ ((Assert ℕn ~ T BY (RelRST THEN Auto)) THEN RepeatFor 2 (D -1)) }
1
1. [T] : Type
2. n : ℕ
3. T ~ ℕn
4. f : ℕn ⟶ T
5. Inj(ℕn;T;f)
6. Surj(ℕn;T;f)
⊢ ∃f:ℕn ⟶ T. Surj(ℕn;T;f)
Latex:
Latex:
1. [T] : Type
2. n : \mBbbN{}
3. T \msim{} \mBbbN{}n
\mvdash{} \mexists{}f:\mBbbN{}n {}\mrightarrow{} T. Surj(\mBbbN{}n;T;f)
By
Latex:
((Assert \mBbbN{}n \msim{} T BY (RelRST THEN Auto)) THEN RepeatFor 2 (D -1))
Home
Index