infinite_of_injOn_mapsTo — Mathlib

English

If f is injective on s and maps s into t, and s is infinite, then t is infinite.

Русский

Если f инъективна на s и отображает s в t, и s бесконечно, то t бесконечно.

LaTeX

$$$ (\operatorname{InjOn}(f,s)) \land (\operatorname{MapsTo}(f,s,t)) \land s.Infinite \Rightarrow t.Infinite $$$

Lean4

theorem infinite_of_injOn_mapsTo {s : Set α} {t : Set β} {f : α → β} (hi : InjOn f s) (hm : MapsTo f s t)
    (hs : s.Infinite) : t.Infinite :=
  ((infinite_image_iff hi).2 hs).mono (mapsTo_iff_image_subset.mp hm)

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