rightInverse_of_injective — Mathlib

English

If f is left inverse of g and f is injective, then there is a right inverse f ⟂ g.

Русский

Если f является левым обратным для g и f инъективна, тогда существует правый обратный f к g.

LaTeX

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

Lean4

theorem rightInverse_of_injective {f : α → β} {g : β → α} (h : LeftInverse f g) (hf : Injective f) : RightInverse f g :=
  fun x ↦ hf <| h (f x)

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