topologicalClosure_toSubalgebra_comm

English

For a StarSubalgebra s, the underlying Subalgebra of its topologicalClosure is identical to the topologicalClosure of its underlying Subalgebra.

Русский

Для подалгебры StarSubalgebra s основанная как Subalgebra топологическаяClosure совпадает с топологическим замыканием соответствующей подалгебры.

LaTeX

$$$\mathrm{toSubalgebra}(s^{\top}) = (\mathrm{toSubalgebra}(s))^{\top}$$$

Lean4

theorem topologicalClosure_toSubalgebra_comm (s : StarSubalgebra R A) :
    s.topologicalClosure.toSubalgebra = s.toSubalgebra.topologicalClosure :=
  SetLike.coe_injective rfl

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