mem_fixedPoints — Mathlib

English

For any a ∈ α, a ∈ fixedPoints M α iff ∀ m ∈ M, m • a = a.

Русский

Для любого a ∈ α верно: a принадлежит fixedPoints M α тогда и только тогда, когда ∀ m ∈ M, m • a = a.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem mem_fixedPoints {a : α} : a ∈ fixedPoints M α ↔ ∀ m : M, m • a = a :=
  Iff.rfl

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