topologicalClosure — Mathlib

English

The topological closure of a non-unital subalgebra is itself a non-unital subalgebra.

Русский

Топологическое замыкание ненулевой подалгебры само является ненулевой подалгеброй.

LaTeX

$$NonUnitalSubalgebra.topologicalClosure$$

Lean4

/-- The (topological) closure of a non-unital subalgebra of a non-unital topological algebra is
itself a non-unital subalgebra. -/
def topologicalClosure (s : NonUnitalSubalgebra R A) : NonUnitalSubalgebra R A :=
  { s.toNonUnitalSubsemiring.topologicalClosure, s.toSubmodule.topologicalClosure with
    carrier := _root_.closure (s : Set A) }

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