unique — Mathlib

English

If two right adjoints exist for the same f, they are equal.

Русский

Если у одной функции f есть две правые сопряжённые g1,g2, то g1=g2.

LaTeX

$$$\\forall f\\ g_1\\ g_2,\\ IsOrderRightAdjoint f g_1 \\to IsOrderRightAdjoint f g_2 \\to g_1=g_2.$$$

Lean4

protected theorem unique [PartialOrder α] [Preorder β] {f : α → β} {g₁ g₂ : β → α} (h₁ : IsOrderRightAdjoint f g₁)
    (h₂ : IsOrderRightAdjoint f g₂) : g₁ = g₂ :=
  funext fun y => (h₁ y).unique (h₂ y)

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