isClosed

Mathlib.Topology.Algebra.StarSubalgebra

URI: https://scilib.ai/kg/mathlib#StarAlgebra.elemental.isClosed

English

For every x, the elemental subalgebra generated by x is closed as a subset of A.

Русский

Для каждого элемента x подалгебра elemental(R,x) замкнута как подмножество A.

LaTeX

$$IsClosed (elemental R x : Set A)$$

Lean4

theorem isClosed (x : A) : IsClosed (elemental R x : Set A) :=
  isClosed_closure

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru