of_injOn — Mathlib

English

If a set maps into another finite set with an injective map, the domain is finite.

Русский

Если отображение сфере в конечное множество и инъективно на исходном множестве, то исходное множество конечно.

LaTeX

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

Lean4

theorem of_injOn {f : α → β} {s : Set α} {t : Set β} (hm : MapsTo f s t) (hi : InjOn f s) (ht : t.Finite) : s.Finite :=
  .of_finite_image (ht.subset (image_subset_iff.mpr hm)) hi

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