topologicalClosure_minimal — Mathlib

English

The topological closure of the subalgebra generated by a set is contained in the centralizer of the centralizer of that set.

Русский

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

LaTeX

$$$\big( \mathrm{adjoin}_R(s) \big)_{topologicalClosure} \le \mathrm{centralizer}_R\big( \mathrm{centralizer}_R(s) \big)$$$

Lean4

theorem topologicalClosure_minimal {s t : Subalgebra R A} (h : s ≤ t) (ht : IsClosed (t : Set A)) :
    s.topologicalClosure ≤ t :=
  closure_minimal h ht

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