injective_iff_periodicPts_eq_univ

English

For finite α, f is injective if and only if periodicPts f equals the whole set univ (i.e., every point is periodic).

Русский

Для конечного множества α отображение f инъективно тогда и только тогда, когда periodicPts f совпадает с всесто univ (то есть каждая точка периодична).

LaTeX

$$$\operatorname{Injective}(f) \iff \mathrm{periodicPts}(f) = \mathrm{univ}$$$

Lean4

theorem injective_iff_periodicPts_eq_univ [Finite α] : Injective f ↔ periodicPts f = univ :=
  by
  refine ⟨fun h ↦ eq_univ_iff_forall.mpr h.mem_periodicPts, fun h ↦ ?_⟩
  rw [Finite.injective_iff_surjective, ← range_eq_univ, ← univ_subset_iff, ← h]
  apply periodicPts_subset_range

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