centralizer_centralizer_centralizer

English

S is contained in the double centralizer of S: S ⊆ centralizer(centralizer(S)).

Русский

S ⊆ centralizer(centralizer(S)).

LaTeX

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

Lean4

@[to_additive (attr := simp) addCentralizer_addCentralizer_addCentralizer]
theorem centralizer_centralizer_centralizer (S : Set M) : S.centralizer.centralizer.centralizer = S.centralizer :=
  by
  refine Set.Subset.antisymm ?_ Set.subset_centralizer_centralizer
  intro x hx
  rw [Set.mem_centralizer_iff]
  intro y hy
  rw [Set.mem_centralizer_iff] at hx
  exact hx y <| Set.subset_centralizer_centralizer hy

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