instHasForget — Mathlib

English

There is a Forgetful functor from DiscreteContAction V G to ContAction V G, forgetting the discreteness constraint.

Русский

Существует функтор забывания из DiscreteContAction V G в ContAction V G, забывающий условие дискретности.

LaTeX

$$$\\mathrm{HasForget} (\\mathrm{DiscreteContAction} V G) := \\mathrm{FullSubcategory}.hasForget(\\mathrm{IsDiscrete}(V := V)(G := G)).$$$

Lean4

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

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