English
If a point a lies in s, then its orbit under fixingSubgroup M sᶜ is contained in s.
Русский
Если a ∈ s, то орбита a под fixingSubgroup M sᶜ содержится в s.
LaTeX
$$$a \\in s \\Rightarrow \\mathrm{orbit}(\\mathrm{fixingSubgroup}(M,s^c),a) \\subseteq s$$$
Lean4
/-- `φ`-equivariant functions `X → Y`,
where `φ : M → N`, where `M` and `N` act additively on `X` and `Y` respectively
We use the same notation as for multiplicative actions, as conflicts are unlikely. -/
@[term_parser 1000]
public meta def «AddActionHomLocal≺» : Lean.TrailingParserDescr✝ :=
ParserDescr.trailingNode✝ `«AddActionHomLocal≺» 25 0
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " →ₑ[") (ParserDescr.cat✝ `term 25))
(ParserDescr.symbol✝ "] "))
(ParserDescr.cat✝ `term 0))
