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 -2) }

1
1. Type
2. : ℕ
3. List
4. : ℕ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