---

Step * 1 1 of Lemma finite-function


1. S : Type
2. n : ℕ
3. S ~ ℕn
4. f : s:S ⟶ ℕ
⊢ ∃n:ℕ. s:S ⟶ ℕf s ~ ℕn
BY
{ ((Assert ℕn ~ S BY (RelRST THEN Auto)) THEN D -1) }

1
1. S : Type
2. n : ℕ
3. S ~ ℕn
4. f : s:S ⟶ ℕ
5. f1 : ℕn ⟶ S
6. Bij(ℕn;S;f1)
⊢ ∃n:ℕ. s:S ⟶ ℕf s ~ ℕn

---

Latex:

---

Latex:

1.  S  :  Type
2.  n  :  \mBbbN{}
3.  S  \msim{}  \mBbbN{}n
4.  f  :  s:S  {}\mrightarrow{}  \mBbbN{}
\mvdash{}  \mexists{}n:\mBbbN{}.  s:S  {}\mrightarrow{}  \mBbbN{}f  s  \msim{}  \mBbbN{}n


By

---

Latex:
((Assert  \mBbbN{}n  \msim{}  S  BY  (RelRST  THEN  Auto))  THEN  D  -1)

---

Home Index