English
For a group G acting on α and β, a subset s ⊆ α supports b ∈ β if every g that fixes all elements of s pointwise also fixes b.
Русский
Пусть G действует на X и Y. Набор s ⊆ X поддерживает b ∈ Y, если каждый элемент g, фиксирующий каждый элемент s по отдельности, фиксирует и b.
LaTeX
$$$ \\text{Supports}(G,s,b) := \\forall g:\\,G,\\, (\\forall a:\\,a\\in s \\rightarrow g\\cdot a = a) \\rightarrow g\\cdot b = b $$$
Lean4
/-- A set `s` supports `b` if `g • b = b` whenever `g • a = a` for all `a ∈ s`. -/
@[to_additive /-- A set `s` supports `b` if `g +ᵥ b = b` whenever `g +ᵥ a = a` for all `a ∈ s`. -/
]
def Supports (s : Set α) (b : β) :=
∀ g : G, (∀ ⦃a⦄, a ∈ s → g • a = a) → g • b = b
