mathlib3 documentation

data.set.pointwise.support

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 : β γ) :
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 : β γ) :
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