instHasForget₂ContAction — Mathlib

English

There is a HasForget₂ functor from DiscreteContAction V G to ContAction V G, reflecting the forgetful relation through the discrete subcategory.

Русский

Существует функтор HasForget₂ из DiscreteContAction V G в ContAction V G, отражающий забывательное отношение через дискретную подкатегорию.

LaTeX

$$$\\text{HasForget₂} (\\mathrm{DiscreteContAction} V G) (\\mathrm{ContAction} V G)$$$

Lean4

instance : HasForget₂ (DiscreteContAction V G) (ContAction V G) :=
  FullSubcategory.hasForget₂ (IsDiscrete (V := V) (G := G))

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