mulSupport_comp_inv_smul — Mathlib

English

For a group acting on β and a function f:β→γ, translating the input by c⁻¹ shifts the support by c: the support of f ∘ (c⁻¹) equals c times the support of f.

Русский

Пусть группа действует на β и f:β→γ. Смещение аргумента на c⁻¹ перемещает опору: опора функции f( c⁻¹•x ) равна c•opora(f).

LaTeX

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

Lean4

theorem mulSupport_comp_inv_smul [One γ] (c : α) (f : β → γ) : (mulSupport fun x ↦ f (c⁻¹ • x)) = c • mulSupport f :=
  by
  ext x
  simp only [mem_smul_set_iff_inv_smul_mem, mem_mulSupport]
    /- Note: to_additive also automatically translates `SMul` to `VAdd`, so we give the additive version
    manually. -/

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