Theorems · Definition · Lie groups

TopRep.of

{k : Type u} →
  {G : Type v} →
    {X : Type w} →
      [inst : TopologicalSpace k] →
        [inst_1 : Ring k] →
          [inst_2 : Monoid G] →
            [inst_3 : AddCommGroup X] →
              [inst_4 : Module k X] →
                [inst_5 : TopologicalSpace X] →
                  [inst_6 : IsTopologicalAddGroup X] → [ContinuousSMul k X] → ContRepresentation k G X → TopRep k G

The object in the category of topological representations associated to a type equipped with a continuous representation. This is the preferred way to construct a term of TopRep k G.

Defined in

Mathlib.RepresentationTheory.Continuous.TopRep

Cited by

12 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms

Assumes

TopologicalSpaceRingMonoidAddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupContinuousSMul