isClosed

Mathlib.Topology.Algebra.NonUnitalStarAlgebra

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

English

For each x, the underlying set of elemental_R(x) is a closed subset of A.

Русский

Каждое множество, лежащее в элементальной подпалгебре, замкнуто в A.

LaTeX

$$$\\text{IsClosed}(\\operatorname{elemental}_R(x))$$$

Lean4

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

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

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

Разделы

Аффилиация

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