Documentation

Mathlib.Data.Set.Pointwise.Support

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 : βγ) :
theorem support_comp_inv_smul {α : Type u_3} {β : Type u_2} {γ : Type u_1} [inst : Group α] [inst : MulAction α β] [inst : Zero γ] (c : α) (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 : βγ) :
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 : βγ) :