isClosed_range

Mathlib.Topology.Algebra.Module.LinearMap

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.IsIdempotentElem.isClosed_range

← MathLib Explorer

English

If p is idempotent and M is a T1 space, then the range of p is closed.

Русский

Если p идемпотентно и M является T1 пространством, то образ p замкнут.

LaTeX

$$$\text{IsIdempotentElem}(p) \Rightarrow \text{IsClosed}(\operatorname{range}(p))$$$

Lean4

theorem isClosed_range [T1Space M] {p : M →L[R] M} (hp : IsIdempotentElem p) : IsClosed (LinearMap.range p : Set M) :=
  hp.range_eq_ker ▸ isClosed_ker (1 - p)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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