splittingOfFunOnFintypeSurjective_injective

English

The splitting map is injective, i.e., it has trivial kernel, under finite α and surjective f.

Русский

Расщепляющее отображение инъективно при конечном α и сюръективности f.

LaTeX

$$$\text{splittingOfFunOnFintypeSurjective}$ is injective$$

Lean4

theorem splittingOfFunOnFintypeSurjective_injective [Finite α] (f : M →ₗ[R] α → R) (s : Surjective f) :
    Injective (splittingOfFunOnFintypeSurjective f s) :=
  (leftInverse_splittingOfFunOnFintypeSurjective f s).injective

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