support_comp_inv_smul — Mathlib

English

If γ has a zero and c acts on α, then translating the input by c⁻¹ shifts the support of f accordingly: the support of f(c⁻¹•x) equals c•support f.

Русский

Если имеется нуль в γ и действует c на α, перенос аргумента на c⁻¹ сдвигает опору функции: опора f(c⁻¹•x) равна c•опора f.

LaTeX

$$$\\operatorname{support}\\bigl(\\lambda x. f(c^{-1}\\cdot x)\\bigr) = c\\cdot \\operatorname{support}(f)$$$

Lean4

theorem support_comp_inv_smul [Zero γ] (c : α) (f : β → γ) : (support fun x ↦ f (c⁻¹ • x)) = c • support f :=
  by
  ext x
  simp only [mem_smul_set_iff_inv_smul_mem, mem_support]

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