centralizer_coe_sup — Mathlib

English

The centralizer of the sup (join) of a family of subalgebras equals the infimum (intersection) of the centralizers: C_R(⊔_i S_i) = ⊓_i C_R(S_i).

Русский

Центральизатор объединения семьи подалгебр равен пересечению центральизаторов: C_R(⊔_i S_i) = ⊓_i C_R(S_i).

LaTeX

$$$\operatorname{centralizer}_R\bigl(\big(\!\big\langle S \bigr\rangle)\bigr) = \bigwedge_i \operatorname{centralizer}_R(S_i)$$$

Lean4

theorem centralizer_coe_sup (S T : Subalgebra R A) :
    centralizer R ((S ⊔ T : Subalgebra R A) : Set A) = centralizer R S ⊓ centralizer R T :=
  eq_of_forall_le_iff fun K ↦ by simp_rw [le_centralizer_iff, sup_le_iff, le_inf_iff, K.le_centralizer_iff]

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