comp_smul — Mathlib

English

If HasCompactMulSupport f, then HasCompactMulSupport (λ x, f (c • x)) for c ≠ 0.

Русский

Если f имеет компактную мультиподдержку, то f(c • x) имеет компактную мультиподдержку.

LaTeX

$$$HasCompactMulSupport (\lambda x, f (c \cdot x))$$$

Lean4

theorem comp_smul {β : Type*} [One β] {f : α → β} (h : HasCompactMulSupport f) {c : G₀} (hc : c ≠ 0) :
    HasCompactMulSupport fun x => f (c • x) :=
  h.comp_homeomorph (Homeomorph.smulOfNeZero c hc)

Похожие утверждения