infinite_range_of_injective — Mathlib

English

If α is infinite and f is injective, then the range of f is infinite.

Русский

Если α бесконечен и f инъективна, то образ f бесконечен.

LaTeX

$$$ [\text{Infinite}(\alpha)] \land \operatorname{Injective}(f) \Rightarrow (\operatorname{range}(f)).Infinite $$$

Lean4

theorem infinite_range_of_injective [Infinite α] {f : α → β} (hi : Injective f) : (range f).Infinite :=
  by
  rw [← image_univ, infinite_image_iff hi.injOn]
  exact infinite_univ

Похожие утверждения