topologicalClosure — Mathlib

English

The topological closure of a subalgebra is a subalgebra whose carrier is the closure of the original carrier.

Русский

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

LaTeX

$$carrier( s.topologicalClosure ) = closure( carrier(s) )$$

Lean4

/-- The topological closure of a subalgebra -/
def _root_.Subalgebra.topologicalClosure (s : Subalgebra R A) : Subalgebra R A
    where
  toSubsemiring := s.toSubsemiring.topologicalClosure
  algebraMap_mem'
    r :=
    by
    simp only [Subsemiring.coe_carrier_toSubmonoid, Subsemiring.topologicalClosure_coe, Subalgebra.coe_toSubsemiring]
    apply subset_closure
    exact algebraMap_mem s r

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