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


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

1
1. Type
2. : ℕ
3. ~ ℕn
4. s:S ⟶ ℕ
5. f1 : ℕn ⟶ S
6. Bij(ℕn;S;f1)
7. i:ℕn ⟶ ℕf1[i] ~ ℕΠ(f f1[i] i < n)
⊢ Bij(s:S ⟶ ℕs;i:ℕn ⟶ ℕ(f1 i);λg,i. (g (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{}  s:S  {}\mrightarrow{}  \mBbbN{}f  s  \msim{}  i:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}f  (f1  i)


By


Latex:
(D  0  With  \mkleeneopen{}\mlambda{}g,i.  (g  (f1  i))\mkleeneclose{}    THEN  Auto)




Home Index