instIsIsoδᵣ

Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.RightLinear.instIsIsoδᵣ

English

δᵣ is an isomorphism for D and D', i.e., δᵣ F d c is an isomorphism.

Русский

δᵣ для D и D' является изоморфизмом: δᵣ F d c — изоморфизм.

LaTeX

$$$\text{IsIso}(\delta^{\mathrm{r}} F d c)$$$

Lean4

instance : IsIso (δᵣ F d c) :=
  Iso.isIso_inv (μᵣIso F d c)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru