instIsRightAdjointCoindFunctor — Mathlib

English

The coinduction functor along φ is a right adjoint to the restriction functor along φ; as an instance, it has the property of being a right adjoint.

Русский

Функтор коиндукции вдоль φ является правым соседом ограничения вдоль φ; как экземпляр, обладает свойством быть правым соседом.

LaTeX

$$$\mathrm{Res}_\phi \dashv \mathrm{coindFunctor}_k\phi$$$

Lean4

noncomputable instance : (coindFunctor k φ).IsRightAdjoint :=
  (resCoindAdjunction k φ).isRightAdjoint

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