---

Step * of Lemma cardinality-le-no_repeats-length

∀[T:Type]. ∀[k:ℕ]. ∀[L:T List].  (||L|| ≤ k) supposing (no_repeats(T;L) and |T| ≤ k)
BY
{ (Auto THEN D -2) }

1
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

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[k:\mBbbN{}].  \mforall{}[L:T  List].    (||L||  \mleq{}  k)  supposing  (no\_repeats(T;L)  and  |T|  \mleq{}  k)


By

---

Latex:
(Auto  THEN  D  -2)

---

Home Index