coe_centralizer_centralizer — Mathlib

English

The centralizer of the centralizer of s, when viewed as a Set, equals the centralizer of s ∪ star s.

Русский

Централизатор централизатора множества s равен централизатору s ∪ star s.

LaTeX

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

Lean4

theorem coe_centralizer_centralizer (s : Set A) :
    (centralizer R (centralizer R s : Set A)) = (s ∪ star s).centralizer.centralizer := by
  rw [coe_centralizer, StarMemClass.star_coe_eq, Set.union_self, coe_centralizer]

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