English
If a function f: ℕ → α maps the initial segment {0,...,n-1} into s and is injective on that segment, then n ≤ |s|.
Русский
Если функция f: ℕ → α отображает начальный отрезок в s и инъективна на этом отрезке, то n ≤ |s|.
LaTeX
$$If ∀ i < n, f(i) ∈ s and ∀ i < n ∀ j < n, f(i) = f(j) → i = j, then n ≤ |s|$$
Lean4
/-- See also `Finset.card_le_card_of_injOn`, which is a more general version of this lemma.
TODO: consider deprecating, since this is just a special case of `Finset.card_le_card_of_injOn`.
-/
theorem le_card_of_inj_on_range (f : ℕ → α) (hf : ∀ i < n, f i ∈ s) (f_inj : ∀ i < n, ∀ j < n, f i = f j → i = j) :
n ≤ #s :=
calc
n = #(range n) := (card_range n).symm
_ ≤ #s := card_le_card_of_injOn f (by simpa [Set.MapsTo, mem_range] using hf) (by simpa)
