English
If a function f: G → α has compact support and is continuous, then either f ≡ 0 or G is locally compact.
Русский
Если функция f: G → α имеет компактную опору и непрерывна, то либо f тождественно равна нулю, либо G локально компактна.
LaTeX
$$$\\forall f: G \\to \\alpha,\\ \\text{HasCompactSupport}(f) \\wedge \\text{Continuous}(f) \\Rightarrow (f = 0 \\lor \\text{LocallyCompactSpace}(G))$$$
Lean4
/-- 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. -/
@[to_additive /-- If a function defined on a topological additive group has a support contained in a compact
set, then either the function is trivial or the group is locally compact. -/
]
theorem eq_zero_or_locallyCompactSpace_of_support_subset_isCompact_of_group [TopologicalSpace α] [Zero α] [T1Space α]
{f : G → α} {k : Set G} (hk : IsCompact k) (hf : support f ⊆ k) (h'f : Continuous f) :
f = 0 ∨ LocallyCompactSpace G := by
refine or_iff_not_imp_left.mpr fun h => ?_
simp_rw [funext_iff, Pi.zero_apply] at h
push_neg at h
obtain ⟨x, hx⟩ : ∃ x, f x ≠ 0 := h
have : k ∈ 𝓝 x := mem_of_superset (h'f.isOpen_support.mem_nhds hx) hf
exact IsCompact.locallyCompactSpace_of_mem_nhds_of_group hk this
