Theorems · Theorem · Lie groups

HasCompactSupport.eq_zero_or_locallyCompactSpace_of_group

∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G]
  [inst_3 : TopologicalSpace α] [inst_4 : Zero α] [T1Space α] {f : G → α},
  HasCompactSupport f → Continuous f → f = 0 ∨ LocallyCompactSpace G

If a function defined on a topological group has compact support, then either the function is trivial or the group is locally compact.

Defined in

Mathlib.Topology.Algebra.Group.Pointwise

Cited by

3 results in Mathlib

Foundations

Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceGroupIsTopologicalGroupTopologicalSpaceZeroT1Space