denseRange

Mathlib.Topology.Continuous

URI: https://scilib.ai/kg/mathlib#Function.Surjective.denseRange

English

The identity map id: X → X has dense range.

Русский

Тождественное отображение id: X → X имеет плотное множество образа.

LaTeX

$$$\\text{DenseRange}(\\mathrm{id}:{X\\to X}).$$$

Lean4

/-- A surjective map has dense range. -/
theorem denseRange (hf : Function.Surjective f) : DenseRange f := fun x => by simp [hf.range_eq]

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

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

Разделы

Аффилиация

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