nonUnitalCommRingTopologicalClosure

English

If x ∈ s and s is closed, then the elemental subalgebra generated by x is contained in s: elemental(R, x) ≤ s.

Русский

Если x ∈ s и s замкнута, то элементарная подалгебра, порожденная x, содержится в s: elemental(R, x) ≤ s.

LaTeX

$$$\text{elemental}(R,x) \le s$ при условии $x \in s$ и IsClosed(s)$$$

Lean4

/-- If a non-unital subalgebra of a non-unital topological algebra is commutative, then so is its
topological closure.

See note [reducible non-instances]. -/
abbrev nonUnitalCommRingTopologicalClosure [T2Space A] (s : NonUnitalSubalgebra R A) (hs : ∀ x y : s, x * y = y * x) :
    NonUnitalCommRing s.topologicalClosure :=
  { s.topologicalClosure.toNonUnitalRing, s.toSubsemigroup.commSemigroupTopologicalClosure hs with }

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