centralizer_eq_top_iff_subset — Mathlib

English

For a subset S of a semigroup M, centralizer S equals the universal set if and only if S is contained in the center of M.

Русский

Для подмножества S полугруппы M центральизатор S равен все множество тогда и только тогда, когда S ⊆ центр M.

LaTeX

$$$ \mathrm{centralizer}(S) = \mathrm{univ} \;\Leftrightarrow\; S \subseteq \mathrm{center}(M) $$$

Lean4

@[to_additive (attr := simp) addCentralizer_eq_top_iff_subset]
theorem centralizer_eq_top_iff_subset : centralizer S = Set.univ ↔ S ⊆ center M :=
  eq_top_iff.trans <|
    ⟨fun h _ hx ↦ Semigroup.mem_center_iff.mpr fun _ ↦ by rw [h trivial _ hx], fun h _ _ _ hm ↦ (h hm).comm _⟩

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