denseRange_val

Mathlib.Topology.Continuous

URI: https://scilib.ai/kg/mathlib#Dense.denseRange_val

English

If s is dense in X, then the inclusion from s to X has dense range.

Русский

Плотность множества s в X значит плотность образа включения s в X.

LaTeX

$$$\\text{Dense}(s) \\Rightarrow \\text{DenseRange}((\\uparrow):s\\to X)$$$

Lean4

theorem denseRange_val (h : Dense s) : DenseRange ((↑) : s → X) :=
  denseRange_subtype_val.2 h

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

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

Разделы

Аффилиация

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