centralizer_union — Mathlib

English

The centralizer of a union equals the intersection of the centralizers: centralizer(S ∪ T) = centralizer(S) ∩ centralizer(T).

Русский

Централизатор объединения равен пересечению централизаторов: centralizer(S ∪ T) = centralizer(S) ∩ centralizer(T).

LaTeX

$$$ \mathrm{centralizer}(S \cup T) = \mathrm{centralizer}(S) \cap \mathrm{centralizer}(T) $$$

Lean4

@[to_additive addCentralizer_union]
theorem centralizer_union : centralizer (S ∪ T) = centralizer S ∩ centralizer T := by
  simp [centralizer, or_imp, forall_and, setOf_and]

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