centralizer_coe_iSup — Mathlib

English

For a family of subalgebras S_i, the centralizer of their iSup is the iInf of their centralizers: C_R(iSup_i S_i) = iInf_i C_R(S_i).

Русский

Центральизатор iSup семейства подалгебр равен iInf центральизаторов: C_R(iSup_i S_i) = iInf_i C_R(S_i).

LaTeX

$$$\operatorname{centralizer}_R\Bigl(\operatorname{instSetLike.coe}\bigl(iSup\, S\bigr)\Bigr) = \bigl(iInf\, i, \operatorname{centralizer}_R(S_i)\bigr)$$$

Lean4

theorem centralizer_coe_iSup {ι : Sort*} (S : ι → Subalgebra R A) :
    centralizer R ((⨆ i, S i : Subalgebra R A) : Set A) = ⨅ i, centralizer R (S i) :=
  eq_of_forall_le_iff fun K ↦ by simp_rw [le_centralizer_iff, iSup_le_iff, le_iInf_iff, K.le_centralizer_iff]

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