leftInverse_splittingOfFunOnFintypeSurjective

English

The splitting map is a left-inverse of f: M → α → R when α is finite and f is surjective.

Русский

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

LaTeX

$$$\text{LeftInverse} (f) (f.splittingOfFunOnFintypeSurjective) = \mathrm{Id}$$$

Lean4

theorem leftInverse_splittingOfFunOnFintypeSurjective [Finite α] (f : M →ₗ[R] α → R) (s : Surjective f) :
    LeftInverse f (splittingOfFunOnFintypeSurjective f s) := fun g =>
  LinearMap.congr_fun (splittingOfFunOnFintypeSurjective_splits f s) g

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