surjOn_iff_bijOn_of_mapsTo — Mathlib

English

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

Русский

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

LaTeX

$$$\mathrm{SurjOn}(f,s,s) \land \mathrm{MapsTo}(f,s,s) \Rightarrow \mathrm{BijOn}(f,s,s) \quad\text{and}\quad \mathrm{SurjOn}(f,s,s) \iff \mathrm{BijOn}(f,s,s)$$$

Lean4

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

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