injOn_iff_bijOn_of_mapsTo — Mathlib

English

For a finite set s and MapsTo f s s, InjOn f s is equivalent to BijOn f s s.

Русский

Для конечного множества s и отображения f, injOn эквивалентно bijOn.

LaTeX

$$$\mathrm{InjOn}(f,s) \iff \mathrm{BijOn}(f,s,s)$ (при условии $\mathrm{MapsTo}(f,s,s)$ и $s$ конечно)$$

Lean4

theorem injOn_iff_bijOn_of_mapsTo (hs : s.Finite) (hm : MapsTo f s s) : InjOn f s ↔ BijOn f s s :=
  by
  refine ⟨fun h ↦ ⟨hm, h, ?_⟩, BijOn.injOn⟩
  have : Finite s := finite_coe_iff.mpr hs
  exact hm.restrict_surjective_iff.mp (Finite.injective_iff_surjective.mp <| hm.restrict_inj.mpr h)

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