Step
*
1
of Lemma
finite-function-equipollent
1. n : ℕ+
2. [F] : ℕn ⟶ Type
⊢ i:ℕn ⟶ F[i] ~ i:ℕn - 1 ⟶ F[i] × F[n - 1]
BY
{ (With ⌜λf.<f, f (n - 1)>⌝ (D 0)⋅ THEN Auto) }
1
1. n : ℕ+
2. [F] : ℕn ⟶ Type
⊢ Bij(i:ℕn ⟶ F[i];i:ℕn - 1 ⟶ F[i] × F[n - 1];λf.<f, f (n - 1)>)
Latex:
Latex:
1. n : \mBbbN{}\msupplus{}
2. [F] : \mBbbN{}n {}\mrightarrow{} Type
\mvdash{} i:\mBbbN{}n {}\mrightarrow{} F[i] \msim{} i:\mBbbN{}n - 1 {}\mrightarrow{} F[i] \mtimes{} F[n - 1]
By
Latex:
(With \mkleeneopen{}\mlambda{}f.<f, f (n - 1)>\mkleeneclose{} (D 0)\mcdot{} THEN Auto)
Home
Index