rightInverse_of_surjective — Mathlib

English

If f has a left inverse g and g is surjective, then f has a right inverse g.

Русский

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

LaTeX

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

Lean4

theorem rightInverse_of_surjective {f : α → β} {g : β → α} (h : LeftInverse f g) (hg : Surjective g) :
    RightInverse f g := fun x ↦
  let ⟨y, hy⟩ := hg x;
  hy ▸ congr_arg g (h y)

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