coe_centralizer — Mathlib

English

The underlying set of the centralizer of s matches the centralizer of the star-closure s ∪ s^* as a set.

Русский

Множество, лежащие в основе централизатора s, совпадает с центализатором замыкания s ∪ s^* по множествам.

LaTeX

$$(centralizer R s : Set A) = (s \cup star s).centralizer$$

Lean4

@[simp, norm_cast]
theorem coe_centralizer (s : Set A) : (centralizer R s : Set A) = (s ∪ star s).centralizer :=
  rfl

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