---

Step * 1 1 1 of Lemma cardinality-le-no_repeats-length


1. T : Type
2. k : ℕ
3. L : T List
4. f : ℕk ⟶ T
5. ∀b:T. ∃a:ℕk. ((f a) = b ∈ T)
6. no_repeats(T;L)
7. g : b:T ⟶ ℕk
8. ∀b:T. ((f (g b)) = b ∈ T)
⊢ Inj(ℕ||L||;ℕk;λi.(g L[i]))
BY
{ ((D 0 THEN Reduce 0) THEN Auto) }

1
1. T : Type
2. k : ℕ
3. L : T List
4. f : ℕk ⟶ T
5. ∀b:T. ∃a:ℕk. ((f a) = b ∈ T)
6. no_repeats(T;L)
7. g : b:T ⟶ ℕk
8. ∀b:T. ((f (g b)) = b ∈ T)
9. a1 : ℕ||L||
10. a2 : ℕ||L||
11. (g L[a1]) = (g L[a2]) ∈ ℕk
⊢ a1 = a2 ∈ ℕ||L||

---

Latex:

---

Latex:

1.  T  :  Type
2.  k  :  \mBbbN{}
3.  L  :  T  List
4.  f  :  \mBbbN{}k  {}\mrightarrow{}  T
5.  \mforall{}b:T.  \mexists{}a:\mBbbN{}k.  ((f  a)  =  b)
6.  no\_repeats(T;L)
7.  g  :  b:T  {}\mrightarrow{}  \mBbbN{}k
8.  \mforall{}b:T.  ((f  (g  b))  =  b)
\mvdash{}  Inj(\mBbbN{}||L||;\mBbbN{}k;\mlambda{}i.(g  L[i]))


By

---

Latex:
((D  0  THEN  Reduce  0)  THEN  Auto)

---

Home Index