---

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


1. T : Type
2. k : ℕ
3. L : T List
4. f : ℕk ⟶ T
5. Surj(ℕk;T;f)
6. no_repeats(T;L)
⊢ ||L|| ≤ k
BY
{ ((Unfold `surject` -2 THEN (Skolemize  (-2) `g')) THENA 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)
⊢ ||L|| ≤ k

---

Latex:

---

Latex:

1.  T  :  Type
2.  k  :  \mBbbN{}
3.  L  :  T  List
4.  f  :  \mBbbN{}k  {}\mrightarrow{}  T
5.  Surj(\mBbbN{}k;T;f)
6.  no\_repeats(T;L)
\mvdash{}  ||L||  \mleq{}  k


By

---

Latex:
((Unfold  `surject`  -2  THEN  (Skolemize    (-2)  `g'))  THENA  Auto)

---

Home Index