English
If HasCompactMulSupport f, then HasCompactMulSupport (λ x, f (c • x)) for c ≠ 0.
Русский
Если функция f имеет компактную мультиподдержку, то функция x ↦ f(c • x) тоже имеет компактную мультиподдержку при c ≠ 0.
LaTeX
$$$HasCompactMulSupport (\lambda x, f (c \cdot x))$$$
Lean4
/-- `smul` is a closed map in the second argument.
The lemma that `smul` is a closed map in the first argument (for a normed space over a complete
normed field) is `isClosedMap_smul_left` in `Analysis.Normed.Module.FiniteDimension`. -/
theorem isClosedMap_smul₀ {E : Type*} [Zero E] [MulActionWithZero G₀ E] [TopologicalSpace E] [T1Space E]
[ContinuousConstSMul G₀ E] (c : G₀) : IsClosedMap fun x : E => c • x :=
by
rcases eq_or_ne c 0 with (rfl | hne)
· simp only [zero_smul]
exact isClosedMap_const
· exact (Homeomorph.smulOfNeZero c hne).isClosedMap
