Support of a function composed with a scalar action #
We show that the support of x ↦ f (c⁻¹ • x) is equal to c • support f.
theorem
mulSupport_comp_inv_smul
{α : Type u_3}
{β : Type u_2}
{γ : Type u_1}
[inst : Group α]
[inst : MulAction α β]
[inst : One γ]
(c : α)
(f : β → γ)
:
(Function.mulSupport fun x => f (c⁻¹ • x)) = c • Function.mulSupport f
theorem
support_comp_inv_smul
{α : Type u_3}
{β : Type u_2}
{γ : Type u_1}
[inst : Group α]
[inst : MulAction α β]
[inst : Zero γ]
(c : α)
(f : β → γ)
:
(Function.support fun x => f (c⁻¹ • x)) = c • Function.support f
theorem
mulSupport_comp_inv_smul₀
{α : Type u_2}
{β : Type u_3}
{γ : Type u_1}
[inst : GroupWithZero α]
[inst : MulAction α β]
[inst : One γ]
{c : α}
(hc : c ≠ 0)
(f : β → γ)
:
(Function.mulSupport fun x => f (c⁻¹ • x)) = c • Function.mulSupport f
theorem
support_comp_inv_smul₀
{α : Type u_2}
{β : Type u_3}
{γ : Type u_1}
[inst : GroupWithZero α]
[inst : MulAction α β]
[inst : Zero γ]
{c : α}
(hc : c ≠ 0)
(f : β → γ)
:
(Function.support fun x => f (c⁻¹ • x)) = c • Function.support f