English
If s ⊊ α and f: s → α is surjective, then α is infinite.
Русский
Если s ⊊ α и f: s → α сюрьективно, то α бесконечен.
LaTeX
$$$\\forall s \\subsetneq \\alpha,\\ (f: s \\to \\alpha)\\ Surjective(f) \\Rightarrow Infinite(\\alpha)$$$
Lean4
/-- If `s : Set α` is a proper subset of `α` and `f : α → s` is injective, then `α` is infinite. -/
theorem of_injective_to_set {s : Set α} (hs : s ≠ Set.univ) {f : α → s} (hf : Injective f) : Infinite α :=
of_not_fintype fun h => by
classical
refine lt_irrefl (Fintype.card α) ?_
calc
Fintype.card α ≤ Fintype.card s := Fintype.card_le_of_injective f hf
_ = #s.toFinset := s.toFinset_card.symm
_ < Fintype.card α := Finset.card_lt_card <| by rwa [Set.toFinset_ssubset_univ, Set.ssubset_univ_iff]
