isClosed_nullSubgroup

Mathlib.Analysis.Normed.Group.NullSubmodule

URI: https://scilib.ai/kg/mathlib#isClosed_nullSubgroup

English

The nullSubgroup (kernel of the norm) is closed in the normed group.

Русский

Ядро нормы (нулевая подгруппа) замкнуто в нормированной группе.

LaTeX

$$$\text{IsClosed}(\{x\in M : \|x\| = 0\})$$$

Lean4

@[to_additive]
theorem isClosed_nullSubgroup : IsClosed (nullSubgroup M : Set M) := by
  apply isClosed_singleton.preimage continuous_norm'

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

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

Разделы

Аффилиация

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