self_mem — Mathlib

English

The topological closure of the subalgebra generated by a set s is contained in the centralizer of the centralizer of s.

Русский

Топологическое замыкание подалгебры, сгенерированной множеством s, содержится в центральизаторе двойного центральизатора S.

LaTeX

$$$\overline{\operatorname{adjoin}_R(s)} \le \operatorname{centralizer}_R(\operatorname{centralizer}_R(s))$$$

Lean4

@[simp, aesop safe (rule_sets := [SetLike])]
theorem self_mem (x : A) : x ∈ elemental R x :=
  le_topologicalClosure _ <| self_mem_adjoin_singleton R x

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