structure ContinuousRep (G : Type u_1) [Group G] [TopologicalSpace G] (V : Type u_2) [AddCommGroup V] [Module ℂ V] [TopologicalSpace V] : Type (max u_1 u_2)

• toMonoidHom : G →* V →L[ℂ] V
• continuous_action : Continuous fun (p : G × V) => (self.toMonoidHom p.1) p.2

def ContinuousRep.ofElem {G : Type u_1} [Group G] [TopologicalSpace G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] [TopologicalSpace V] (π : ContinuousRep G V) (g : G) : V →L[ℂ] V

structure ContinuousRep.IsInvariantSubspace {G : Type u_1} [Group G] [TopologicalSpace G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] [TopologicalSpace V] (π : ContinuousRep G V) (W : Submodule ℂ V) : Prop

• isClosed : IsClosed ↑W
• invariant (g : G) (v : V) : v ∈ W → (π.toMonoidHom g) v ∈ W

def ContinuousRep.IsIrreducible {G : Type u_1} [Group G] [TopologicalSpace G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] [TopologicalSpace V] (π : ContinuousRep G V) : Prop

def ContinuousRep.directSum {G : Type u_1} [Group G] [TopologicalSpace G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] [TopologicalSpace V] {W : Type u_3} [AddCommGroup W] [Module ℂ W] [TopologicalSpace W] (π₁ : ContinuousRep G V) (π₂ : ContinuousRep G W) : ContinuousRep G (V × W)

def ContinuousRep.IsUnitary {G : Type u_1} [Group G] [TopologicalSpace G] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (π : ContinuousRep G E) : Prop

def ContinuousRep.IsStronglyContinuous {G : Type u_1} [Group G] [TopologicalSpace G] {V : Type u_4} [NormedAddCommGroup V] [NormedSpace ℂ V] (π : G →* V →L[ℂ] V) : Prop

theorem ContinuousRep.stronglyContinuous_of_continuousRep {G : Type u_1} [Group G] [TopologicalSpace G] {V : Type u_4} [NormedAddCommGroup V] [NormedSpace ℂ V] (ρ : ContinuousRep G V) : IsStronglyContinuous ρ.toMonoidHom

theorem ContinuousRep.continuousRep_of_stronglyContinuous {G : Type u_1} [Group G] [TopologicalSpace G] {V : Type u_4} [NormedAddCommGroup V] [NormedSpace ℂ V] [CompleteSpace V] [SequentialSpace (G × V)] (π : G →* V →L[ℂ] V) (hsc : IsStronglyContinuous π) : Continuous fun (p : G × V) => (π p.1) p.2

theorem ContinuousRep.continuousRep_iff_stronglyContinuous {G : Type u_1} [Group G] [TopologicalSpace G] {V : Type u_4} [NormedAddCommGroup V] [NormedSpace ℂ V] [CompleteSpace V] [SequentialSpace (G × V)] (π : G →* V →L[ℂ] V) : (Continuous fun (p : G × V) => (π p.1) p.2) ↔ IsStronglyContinuous π

structure RepHom {G : Type u_1} [Group G] [TopologicalSpace G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] [TopologicalSpace V] {W : Type u_3} [AddCommGroup W] [Module ℂ W] [TopologicalSpace W] (π₁ : ContinuousRep G V) (π₂ : ContinuousRep G W) : Type (max u_2 u_3)

• toContinuousLinearMap : V →L[ℂ] W
• intertwines (g : G) : self.toContinuousLinearMap.comp (π₁.toMonoidHom g) = (π₂.toMonoidHom g).comp self.toContinuousLinearMap

structure RepEquiv {G : Type u_1} [Group G] [TopologicalSpace G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] [TopologicalSpace V] {W : Type u_3} [AddCommGroup W] [Module ℂ W] [TopologicalSpace W] (π₁ : ContinuousRep G V) (π₂ : ContinuousRep G W) : Type (max u_2 u_3)

• toContinuousLinearEquiv : V ≃L[ℂ] W
• intertwines (g : G) : (↑self.toContinuousLinearEquiv).comp (π₁.toMonoidHom g) = (π₂.toMonoidHom g).comp ↑self.toContinuousLinearEquiv

def RepEquiv.toRepHom {G : Type u_1} [Group G] [TopologicalSpace G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] [TopologicalSpace V] {W : Type u_3} [AddCommGroup W] [Module ℂ W] [TopologicalSpace W] {π₁ : ContinuousRep G V} {π₂ : ContinuousRep G W} (e : RepEquiv π₁ π₂) : RepHom π₁ π₂