English
For any finite type α and any function f: Fin(m) → α with decidable equality, the cardinality of the image (range) is at most m.
Русский
Для любого конечного типа α и любой функции f: Fin(m) → α с DecidableEq, число элементов образа равно m сверху ограничено.
LaTeX
$$$\forall \alpha\ [\text{Fintype }\alpha]\ [\text{DecidableEq }\alpha]\ (f:\mathrm{Fin}(m)\to \alpha)\;\Rightarrow\; \lvert \operatorname{Set.range} f \rvert \le m.$$$
Lean4
/-- Any map from `Fin m` reaches at most `m` different values.
See also `Fintype.card_range_le` for the generalisation to an arbitrary finite type.
-/
theorem card_range_le {α : Type*} [Fintype α] [DecidableEq α] (f : Fin m → α) : Fintype.card (Set.range f) ≤ m := by
simpa using Fintype.card_range_le f
