support_comp_inv_smul₀ — Mathlib

English

Again in the zero-requiring setting, the translated input shifts the support by c, provided the inverse exists and c ≠ 0.

Русский

Снова в условиях с нулём, сдвигая вход на c аналогично, опора смещается на c, если существует обратное и c ≠ 0.

LaTeX

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

Lean4

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

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