DiscreteContAction — Mathlib

English

The DiscreteContAction is the full subcategory of ContAction where the topology on the underlying carrier is discrete.

Русский

DiscreteContAction — это полная подкатегория ContAction состоящая из тех объектов, у которых топология над носителем дискретна.

LaTeX

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

Lean4

/-- The subcategory of `ContAction V G` where the topology is discrete. -/
def DiscreteContAction : Type _ :=
  ObjectProperty.FullSubcategory (IsDiscrete (V := V) (G := G))

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