mem_fixingSubmonoid_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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