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

theorem ContinuousRep.isKFinite_zero {G : Type u_1} [Group G] [TopologicalSpace G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] [TopologicalSpace V] (π : ContinuousRep G V) (K : Subgroup G) : π.IsKFinite K 0

theorem ContinuousRep.isKFinite_add {G : Type u_1} [Group G] [TopologicalSpace G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] [TopologicalSpace V] (π : ContinuousRep G V) (K : Subgroup G) (v w : V) (hv : π.IsKFinite K v) (hw : π.IsKFinite K w) : π.IsKFinite K (v + w)

theorem ContinuousRep.isKFinite_smul {G : Type u_1} [Group G] [TopologicalSpace G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] [TopologicalSpace V] (π : ContinuousRep G V) (K : Subgroup G) (c : ℂ) (v : V) (hv : π.IsKFinite K v) : π.IsKFinite K (c • v)

def ContinuousRep.kFiniteSubspace {G : Type u_1} [Group G] [TopologicalSpace G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] [TopologicalSpace V] (π : ContinuousRep G V) (K : Subgroup G) : Submodule ℂ V

theorem ContinuousRep.mem_kFiniteSubspace {G : Type u_1} [Group G] [TopologicalSpace G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] [TopologicalSpace V] (π : ContinuousRep G V) (K : Subgroup G) (v : V) : v ∈ π.kFiniteSubspace K ↔ π.IsKFinite K v

def ContinuousRep.restrictSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] [TopologicalSpace V] [IsTopologicalGroup G] (π : ContinuousRep G V) (K : Subgroup G) : ContinuousRep (↥K) V

def ContinuousRep.subrepresentation {G : Type u_1} [Group G] [TopologicalSpace G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] [TopologicalSpace V] (π : ContinuousRep G V) (W : Submodule ℂ V) (hW : π.IsInvariantSubspace W) : ContinuousRep G ↥W

def ContinuousRep.IsotypicComponent {G : Type u_1} [Group G] [TopologicalSpace G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] [TopologicalSpace V] [IsTopologicalGroup G] {Wσ : Type u_3} [AddCommGroup Wσ] [Module ℂ Wσ] [TopologicalSpace Wσ] (π : ContinuousRep G V) (K : Subgroup G) (σ : ContinuousRep (↥K) Wσ) : Submodule ℂ V