mem_fixingSubgroup_iff — Mathlib

English

Membership in fixingSubgroup M s is equivalent to fixing every element of s.

Русский

Членство в fixingSubgroup(M,s) эквивалентно фиксации каждого элемента s.

LaTeX

$$$m \\in fixingSubgroup(M,s) \\iff \\forall y \\in s:\\; m \\cdot y = y$$$

Lean4

@[to_additive]
theorem mem_fixingSubgroup_iff {s : Set α} {m : M} : m ∈ fixingSubgroup M s ↔ ∀ y ∈ s, m • y = y :=
  ⟨fun hg y hy => hg ⟨y, hy⟩, fun h ⟨y, hy⟩ => h y hy⟩

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