Theorems · Theorem · Lie groups

eq_zero_or_locallyCompactSpace_of_support_subset_isCompact_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 → α} {k : Set G},
  IsCompact k → Function.support f ⊆ k → Continuous f → f = 0 ∨ LocallyCompactSpace G

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

Defined in

Mathlib.Topology.Algebra.Group.Pointwise

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceGroupIsTopologicalGroupTopologicalSpaceZeroT1Space