isClosed

Mathlib.Analysis.Normed.Ring.Units

URI: https://scilib.ai/kg/mathlib#nonunits.isClosed

English

The set of nonunits is a closed subset in the underlying normed ring.

Русский

Множество неединиц замкнуто в основе нормированного кольца.

LaTeX

$$IsClosed( nonunits R )$$

Lean4

protected theorem isClosed : IsClosed (nonunits R) :=
  Units.isOpen.isClosed_compl

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

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

Разделы

Аффилиация

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