le_centralizer_iff — Mathlib

English

Two subalgebras S, T satisfy S ≤ centralizer T iff T ≤ centralizer S; i.e., mutual centralizers are in a precise dual relation.

Русский

Для подалгебр S и T верно S ≤ C_R(T) тогда и только тогда, когда T ≤ C_R(S).

LaTeX

$$$S \leq \operatorname{centralizer}_R(T) \iff T \leq \operatorname{centralizer}_R(S)$$$

Lean4

theorem le_centralizer_iff (S T : Subalgebra R A) : S ≤ centralizer R T ↔ T ≤ centralizer R S :=
  ⟨fun h t ht _ hs ↦ (h hs t ht).symm, fun h s hs _ ht ↦ (h ht s hs).symm⟩

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