mulSupport_comp_inv_smul₀ — Mathlib

English

In a group-with-zero setting, if c ≠ 0, translating the argument by c⁻¹ yields the same shift for the mulSupport as before.

Русский

В окружении группы с нулём, если c ≠ 0, перенос аргумента на c⁻¹ даёт тот же сдвиг опоры, что и ранее.

LaTeX

$$$\\operatorname{mulSupport}\\bigl(\\lambda x. f(c^{-1}\\cdot x)\\bigr) = c\\cdot \\operatorname{mulSupport}(f)$, при $c \\neq 0$$$

Lean4

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

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