finite_of_finite_preimage — Mathlib

English

If the preimage under f of s is finite and f is injective on s, then s is finite.

Русский

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

LaTeX

$$$\mathrm{Finite}(f^{-1}(s)) \land \mathrm{InjOn}(f,s) \Rightarrow \mathrm{Finite}(s)$$$

Lean4

theorem finite_of_finite_preimage (h : (f ⁻¹' s).Finite) (hs : s ⊆ range f) : s.Finite :=
  by
  rw [← image_preimage_eq_of_subset hs]
  exact Finite.image f h

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