eq_rightInverse — Mathlib

English

Let f: α → β, g1: β → α, g2: β → α. If g1 is a left inverse of f and g2 is a right inverse of f, then g1 = g2.

Русский

Пусть f: α → β, g1: β → α, g2: β → α. Если g1 является левым обратным к f, а g2 — правым обратным к f, то g1 = g2.

LaTeX

$$$ \mathrm{LeftInverse}(g_1,f) \rightarrow \mathrm{RightInverse}(g_2,f) \rightarrow g_1 = g_2 $$$

Lean4

theorem eq_rightInverse {f : α → β} {g₁ g₂ : β → α} (h₁ : LeftInverse g₁ f) (h₂ : RightInverse g₂ f) : g₁ = g₂ :=
  calc
    g₁ = g₁ ∘ f ∘ g₂ := by rw [h₂.comp_eq_id, comp_id]
    _ = g₂ := by rw [← comp_assoc, h₁.comp_eq_id, id_comp]

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