English
If a function has compact support, then either the function is zero or the group is locally compact (same as 195218).
Русский
Если функция имеет компактную опору, то либо функция нулевая, либо группа локально компактна.
LaTeX
$$$\\forall f: G \\to \\alpha,\\ (\\text{HasCompactSupport}(f)) \\Rightarrow (f = 0 \\lor \\text{LocallyCompactSpace}(G))$$$
Lean4
/-- If a function defined on a topological group has compact support, then either
the function is trivial or the group is locally compact. -/
@[to_additive /-- If a function defined on a topological additive group has compact support,
then either the function is trivial or the group is locally compact. -/
]
theorem eq_zero_or_locallyCompactSpace_of_group [TopologicalSpace α] [Zero α] [T1Space α] {f : G → α}
(hf : HasCompactSupport f) (h'f : Continuous f) : f = 0 ∨ LocallyCompactSpace G :=
eq_zero_or_locallyCompactSpace_of_support_subset_isCompact_of_group hf (subset_tsupport f) h'f
