elemental — Mathlib

English

The elemental subalgebra generated by a single element x is the topological closure of the subalgebra adjoin_R({x}).

Русский

Элементальная подалгебра, порождаемая одним элементом x, есть как топологическое замыкание подалгебры, порожденной {x}.

LaTeX

$$$\\operatorname{elemental}_R(x)=\\overline{\\operatorname{adjoin}_R\\{x\\}}.$$$

Lean4

/-- The topological closure of the non-unital star subalgebra generated by a single element. -/
def elemental (x : A) : NonUnitalStarSubalgebra R A :=
  adjoin R { x } |>.topologicalClosure

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