---

Step * 1 1 1 1 1 1 1 of Lemma finite-function


1. S : Type
2. n : ℕ
3. S ~ ℕn
4. f : s:S ⟶ ℕ
5. f1 : ℕn ⟶ S
6. Bij(ℕn;S;f1)
7. i:ℕn ⟶ ℕf o f1[i] ~ ℕΠ(f o f1[i] | i < n)
⊢ Bij(s:S ⟶ ℕf s;i:ℕn ⟶ ℕf (f1 i);λg,i. (g (f1 i)))
BY
{ (RepeatFor 2 (D 0) THEN Auto) }

1
1. S : Type
2. n : ℕ
3. S ~ ℕn
4. f : s:S ⟶ ℕ
5. f1 : ℕn ⟶ S
6. Bij(ℕn;S;f1)
7. i:ℕn ⟶ ℕf o f1[i] ~ ℕΠ(f o f1[i] | i < n)
8. a1 : s:S ⟶ ℕf s
9. a2 : s:S ⟶ ℕf s
10. ((λg,i. (g (f1 i))) a1) = ((λg,i. (g (f1 i))) a2) ∈ (i:ℕn ⟶ ℕf (f1 i))
⊢ a1 = a2 ∈ (s:S ⟶ ℕf s)

2
1. S : Type
2. n : ℕ
3. S ~ ℕn
4. f : s:S ⟶ ℕ
5. f1 : ℕn ⟶ S
6. Bij(ℕn;S;f1)
7. i:ℕn ⟶ ℕf o f1[i] ~ ℕΠ(f o f1[i] | i < n)
8. b : i:ℕn ⟶ ℕf (f1 i)
⊢ ∃a:s:S ⟶ ℕf s. (((λg,i. (g (f1 i))) a) = b ∈ (i:ℕn ⟶ ℕf (f1 i)))

---

Latex:

---

Latex:

1.  S  :  Type
2.  n  :  \mBbbN{}
3.  S  \msim{}  \mBbbN{}n
4.  f  :  s:S  {}\mrightarrow{}  \mBbbN{}
5.  f1  :  \mBbbN{}n  {}\mrightarrow{}  S
6.  Bij(\mBbbN{}n;S;f1)
7.  i:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}f  o  f1[i]  \msim{}  \mBbbN{}\mPi{}(f  o  f1[i]  |  i  <  n)
\mvdash{}  Bij(s:S  {}\mrightarrow{}  \mBbbN{}f  s;i:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}f  (f1  i);\mlambda{}g,i.  (g  (f1  i)))


By

---

Latex:
(RepeatFor  2  (D  0)  THEN  Auto)

---

Home Index