# Support of an element under an action action #

Given an action of a group G on a type α, we say that a set s : Set α supports an element a : α if, for all g that fix s pointwise, g fixes a.

This is crucial in Fourier-Motzkin constructions.

def AddAction.Supports (G : Type u_1) {α : Type u_3} {β : Type u_4} [VAdd G α] [VAdd G β] (s : Set α) (b : β) :

A set s supports b if g +ᵥ b = b whenever g +ᵥ a = a for all a ∈ s.

Equations
• = ∀ (g : G), (∀ ⦃a : α⦄, a sg +ᵥ a = a)g +ᵥ b = b
Instances For
def MulAction.Supports (G : Type u_1) {α : Type u_3} {β : Type u_4} [SMul G α] [SMul G β] (s : Set α) (b : β) :

A set s supports b if g • b = b whenever g • a = a for all a ∈ s.

Equations
• = ∀ (g : G), (∀ ⦃a : α⦄, a sg a = a)g b = b
Instances For
theorem AddAction.supports_of_mem (G : Type u_1) {α : Type u_3} [VAdd G α] {s : Set α} {a : α} (ha : a s) :
theorem MulAction.supports_of_mem (G : Type u_1) {α : Type u_3} [SMul G α] {s : Set α} {a : α} (ha : a s) :
theorem AddAction.Supports.mono {G : Type u_1} {α : Type u_3} {β : Type u_4} [VAdd G α] [VAdd G β] {s : Set α} {t : Set α} {b : β} (h : s t) (hs : ) :
theorem MulAction.Supports.mono {G : Type u_1} {α : Type u_3} {β : Type u_4} [SMul G α] [SMul G β] {s : Set α} {t : Set α} {b : β} (h : s t) (hs : ) :
theorem AddAction.Supports.vadd {G : Type u_1} {H : Type u_2} {α : Type u_3} {β : Type u_4} [] [VAdd G α] [VAdd G β] [] [VAdd H β] [] [] {s : Set α} {b : β} (g : H) (h : ) :
theorem MulAction.Supports.smul {G : Type u_1} {H : Type u_2} {α : Type u_3} {β : Type u_4} [] [SMul G α] [SMul G β] [] [SMul H β] [] [] {s : Set α} {b : β} (g : H) (h : ) :
MulAction.Supports G (g s) (g b)