finite_of_finite_image — Mathlib

English

If s is a subset of α, f : α → β is injective on s, and f[s] is finite, then s is finite.

Русский

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

LaTeX

$$$ (\text{InjOn } f\ s) \land Finite (f'' s) \Rightarrow Finite s $$$

Lean4

theorem finite_of_finite_image (s : Set α) {f : α → β} (h : s.InjOn f) [Finite (f '' s)] : Finite s :=
  Finite.of_equiv _ (Equiv.ofBijective _ h.bijOn_image.bijective).symm

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