instCategory — Mathlib

English

The category DiscreteContAction V G is the full subcategory of ContAction on objects with discrete topology.

Русский

Категория DiscreteContAction V G является полной подкатегорией ContAction на объектах с дискретной топологией.

LaTeX

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

Lean4

instance : Category (DiscreteContAction V G) :=
  ObjectProperty.FullSubcategory.category (IsDiscrete (V := V) (G := G))

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