finite_image_iff — Mathlib

English

If f is injective on s, then f(s) is finite iff s is finite.

Русский

Если f инъективна на s, то образ s под f конечен тогда и только тогда, когда s конечна.

LaTeX

$$$ (f '' s).Finite \\iff s.Finite \\quad \\text{under } (hi : InjOn f s) $$$

Lean4

theorem finite_image_iff {s : Set α} {f : α → β} (hi : InjOn f s) : (f '' s).Finite ↔ s.Finite :=
  ⟨fun h => h.of_finite_image hi, Finite.image _⟩

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