leftInverse_of_surjective — Mathlib

English

If RightInverse f g holds and g is surjective, then f has a LeftInverse g.

Русский

Если RightInverse f g выполняется и g сюръективна, то f имеет левый обратный g.

LaTeX

$$$\text{RightInverse}(f,g) \Rightarrow \operatorname{Surjective}(g) \Rightarrow \operatorname{LeftInverse}(f,g).$$$

Lean4

theorem leftInverse_of_surjective {f : α → β} {g : β → α} : RightInverse f g → Surjective f → LeftInverse f g :=
  LeftInverse.rightInverse_of_surjective

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