closure_range — Mathlib

English

If h is a dense-range map, then closure of range h equals univ.

Русский

Если образ непрерывного отображения плотно насыщает пространство, то замыкание образа равно всему пространству.

LaTeX

$$$\\text{DenseRange}(f) \\Rightarrow \\overline{\\mathrm{range}(f)} = \\mathsf{univ}$$$

Lean4

theorem closure_range (h : DenseRange f) : closure (range f) = univ :=
  h.closure_eq

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