leftInverse_of_injective — Mathlib

English

Let f: α → β and g: β → α. If f ∘ g = id_β and g is injective, then g ∘ f = id_α.

Русский

Пусть f: α → β и g: β → α. Если f ∘ g = id_β и g инъективна, то g ∘ f = id_α.

LaTeX

$$$ (f \circ g = \mathrm{id}_{\beta}) \rightarrow (Injective\ g) \rightarrow (g \circ f = \mathrm{id}_{\alpha}) $$$

Lean4

theorem leftInverse_of_injective {f : α → β} {g : β → α} : RightInverse f g → Injective g → LeftInverse f g :=
  LeftInverse.rightInverse_of_injective

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