subset_centralizer_centralizer — Mathlib

English

Any element of S is contained in the centralizer of the centralizer of S.

Русский

Любой элемент из S принадлежит центральizатору центральizатора S.

LaTeX

$$$ S \subseteq \mathrm{centralizer}(\mathrm{centralizer}(S)) $$$

Lean4

@[to_additive subset_addCentralizer_addCentralizer]
theorem subset_centralizer_centralizer : S ⊆ S.centralizer.centralizer :=
  by
  intro x hx
  simp only [Set.mem_centralizer_iff]
  exact fun y hy => (hy x hx).symm

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