---

Step * 1 1 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)
9. a1 : ℕ||L||
10. a2 : ℕ||L||
11. (g L[a1]) = (g L[a2]) ∈ ℕk
12. L[a1] = L[a2] ∈ T
⊢ a1 = a2 ∈ ℕ||L||
BY
{ (SupposeNot THEN Unfold `no_repeats` 6 THEN InstHyp [⌜a1⌝;⌜a2⌝] 6⋅ THEN Auto) }

---

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)
9.  a1  :  \mBbbN{}||L||
10.  a2  :  \mBbbN{}||L||
11.  (g  L[a1])  =  (g  L[a2])
12.  L[a1]  =  L[a2]
\mvdash{}  a1  =  a2


By

---

Latex:
(SupposeNot  THEN  Unfold  `no\_repeats`  6  THEN  InstHyp  [\mkleeneopen{}a1\mkleeneclose{};\mkleeneopen{}a2\mkleeneclose{}]  6\mcdot{}  THEN  Auto)

---

Home Index