closure_range

Mathlib.Topology.DenseEmbedding

URI: https://scilib.ai/kg/mathlib#IsDenseInducing.closure_range

English

If i is a dense inducing map, then the closure of its range is the whole space.

Русский

Если i — плотное индуциирующее отображение, то замыкание образа i — это вся пространство.

LaTeX

$$$ closure(\\text{range}(i)) = \\; univ $$$

Lean4

theorem closure_range (di : IsDenseInducing i) : closure (range i) = univ :=
  di.dense.closure_range

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

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

Разделы

Аффилиация

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