English
Let s be a star-subalgebra of a topological star-algebra A over a commutative semiring R. Then its topological closure inside A forms a star-subalgebra; in particular, its carrier is the closure of the underlying set of s, and it is closed under addition, multiplication, scalar action, and the star operation.
Русский
Пусть s — звездо-подалгебра в топологической звездоалгебре A над коммутативным полем R. Тогда топологическое замыкание s внутри A образует звездо-подалгебру; в частности, множество, лежащее под ней (carrier), равно замыканию множества s, и оно замкнуто относительно сложения, умножения, скалярного действия и звезды.
LaTeX
$$$\mathrm{topologicalClosure}(s)$ является звездо-подалгеброй в $A$ с носителем $\overline{(s)}$.$$
Lean4
/-- The closure of a star subalgebra in a topological star algebra as a star subalgebra. -/
def topologicalClosure (s : StarSubalgebra R A) : StarSubalgebra R A :=
{ s.toSubalgebra.topologicalClosure with
carrier := closure (s : Set A)
star_mem' := fun ha => map_mem_closure continuous_star ha fun x => (star_mem : x ∈ s → star x ∈ s) }
