---

Step * 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
⊢ a1 = a2 ∈ ℕ||L||
BY
{ (Assert L[a1] = L[a2] ∈ T BY
         (((InstHyp [⌜L[a1]⌝] (-4))⋅ THENA Auto)
          THEN ((InstHyp [⌜L[a2]⌝] (-5))⋅ THENA Auto)
          THEN (HypSubst (-3) (-2))
          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
12. L[a1] = L[a2] ∈ T
⊢ 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)
9.  a1  :  \mBbbN{}||L||
10.  a2  :  \mBbbN{}||L||
11.  (g  L[a1])  =  (g  L[a2])
\mvdash{}  a1  =  a2


By

---

Latex:
(Assert  L[a1]  =  L[a2]  BY
              (((InstHyp  [\mkleeneopen{}L[a1]\mkleeneclose{}]  (-4))\mcdot{}  THENA  Auto)
                THEN  ((InstHyp  [\mkleeneopen{}L[a2]\mkleeneclose{}]  (-5))\mcdot{}  THENA  Auto)
                THEN  (HypSubst  (-3)  (-2))
                THEN  Auto))

---

Home Index