of_finite_image — Mathlib

English

If the image of a set under f is finite and f is injective on the set, then the set is finite.

Русский

Если образ множества под действием f конечен и f инъективен на множестве, то множество конечно.

LaTeX

$$$\mathrm{Finite}(\mathrm{image}(f,s)) \land \mathrm{InjOn}(f,s) \Rightarrow \mathrm{Finite}(s)$$$

Lean4

theorem of_finite_image {s : Set α} {f : α → β} (h : (f '' s).Finite) (hi : Set.InjOn f s) : s.Finite :=
  have := h.to_subtype
  .of_injective _ hi.bijOn_image.bijective.injective

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