le_iff_mem — Mathlib

English

The elemental subalgebra generated by x is contained in the double centralizer of x: it lies inside the centralizer of the centralizer of {x}.

Русский

Элементальная подпалгебра, порождаемая x, содержится во втором центральизаторе x: она лежит внутри центральизатора центральизатора {x}.

LaTeX

$$$\\operatorname{elemental}_R(x) \\le \\operatorname{centralizer}_R(\\operatorname{centralizer}_R(\\{x\\})).$$$

Lean4

theorem le_iff_mem {x : A} {s : NonUnitalStarSubalgebra R A} (hs : IsClosed (s : Set A)) : elemental R x ≤ s ↔ x ∈ s :=
  ⟨fun h ↦ h (self_mem R x), fun h ↦ le_of_mem hs h⟩

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