---

Step * 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)
⊢ ||L|| ≤ k
BY
{ (Using [`f', ⌜λi.(g L[i])⌝] (BLemma `pigeon-hole`)⋅ 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)
⊢ Inj(ℕ||L||;ℕk;λi.(g L[i]))

---

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{}  ||L||  \mleq{}  k


By

---

Latex:
(Using  [`f',  \mkleeneopen{}\mlambda{}i.(g  L[i])\mkleeneclose{}]  (BLemma  `pigeon-hole`)\mcdot{}  THEN  Auto)

---

Home Index