fixedPoints — Mathlib

English

Let M act on α. The fixed points form the subset { a ∈ α | ∀ m ∈ M, m • a = a }.

Русский

Пусть M действует на α. Множество зафиксированных точек состоит из всех a ∈ α таких, что ∀ m ∈ M выполняется m • a = a.

LaTeX

$$$$\\mathrm{fixedPoints}(M, \\alpha) = \\{ a \\in \\alpha \\mid \\forall m \\in M,\\ m \\cdot a = a \\}.$$$$

Lean4

/-- The set of elements fixed under the whole action. -/
@[to_additive /-- The set of elements fixed under the whole action. -/
    ]
def fixedPoints : Set α :=
  {a : α | ∀ m : M, m • a = a}

Похожие утверждения