infinite_range_iff — Mathlib

English

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

Русский

Если f инъективна, то образ f имеет бесконечную мощность тогда и только тогда, когда α бесконечно.

LaTeX

$$$ (\text{Injective } f) \Rightarrow (\operatorname{range}(f)).Infinite \iff \operatorname{Infinite}(\alpha) $$$

Lean4

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

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