denseRange_coe — Mathlib

English

If X is not compact, the natural embedding X → OnePoint X has dense range in the one-point compactification.

Русский

Если X не компактно, естественное вложение X ↪ OnePoint X имеет плотное образующее множество в однопунктной компактфикации.

LaTeX

$$$\\operatorname{DenseRange}(\\iota: X \\to \\mathrm{OnePoint}(X))$, где $\\iota(x)=x$.$$

Lean4

/-- If `X` is not a compact space, then the natural embedding `X → OnePoint X` has dense range.
-/
theorem denseRange_coe [NoncompactSpace X] : DenseRange ((↑) : X → OnePoint X) :=
  by
  rw [DenseRange, ← compl_infty]
  exact dense_compl_singleton _

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