Pigeonhole-like results for Fin

This adapts Pigeonhole-like results from Mathlib.Data.Fintype.Card to the setting where the map has the type f : Fin m → Fin n.

theorem Fin.le_of_injective {m n : ℕ} (f : Fin m → Fin n) (hf : Function.Injective f) : m ≤ n

If we have an injective map from Fin m to Fin n, then m ≤ n. See also Fintype.card_le_of_injective for the generalisation to arbitrary finite types.

theorem Fin.le_of_embedding {m n : ℕ} (f : Fin m ↪ Fin n) : m ≤ n

If we have an embedding from Fin m to Fin n, then m ≤ n. See also Fintype.card_le_of_embedding for the generalisation to arbitrary finite types.

theorem Fin.lt_of_injective_of_notMem {m n : ℕ} (f : Fin m → Fin n) (hf : Function.Injective f) {b : Fin n} (hb : b ∉ Set.range f) : m < n

If we have an injective map from Fin m to Fin n whose image does not contain everything, then m < n. See also Fintype.card_lt_of_injective_of_notMem for the generalisation to arbitrary finite types.

theorem Fin.le_of_surjective {m n : ℕ} (f : Fin m → Fin n) (hf : Function.Surjective f) : n ≤ m

If we have a surjective map from Fin m to Fin n, then m ≥ n. See also Fintype.card_le_of_surjective for the generalisation to arbitrary finite types.

theorem Fin.card_range_le {m : ℕ} {α : Type u_1} [Fintype α] [DecidableEq α] (f : Fin m → α) : Fintype.card ↑(Set.range f) ≤ m

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.