Support of a function composed with a scalar action #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We show that the support of x ↦ f (c⁻¹ • x) is equal to c • support f.
theorem
mul_support_comp_inv_smul
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[group α]
[mul_action α β]
[has_one γ]
(c : α)
(f : β → γ) :
function.mul_support (λ (x : β), f (c⁻¹ • x)) = c • function.mul_support f
theorem
support_comp_inv_smul
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[group α]
[mul_action α β]
[has_zero γ]
(c : α)
(f : β → γ) :
function.support (λ (x : β), f (c⁻¹ • x)) = c • function.support f
theorem
mul_support_comp_inv_smul₀
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[group_with_zero α]
[mul_action α β]
[has_one γ]
{c : α}
(hc : c ≠ 0)
(f : β → γ) :
function.mul_support (λ (x : β), f (c⁻¹ • x)) = c • function.mul_support f
theorem
support_comp_inv_smul₀
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[group_with_zero α]
[mul_action α β]
[has_zero γ]
{c : α}
(hc : c ≠ 0)
(f : β → γ) :
function.support (λ (x : β), f (c⁻¹ • x)) = c • function.support f