denseRange_iff_closure_range — Mathlib

English

If f has dense range, then closure of range f equals the whole space.

Русский

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

LaTeX

$$$\\forall f:\\,X\\to Y,\\ \\text{DenseRange}(f) \\Rightarrow \\overline{\\mathrm{range}(f)} = \\mathsf{univ}$$$

Lean4

theorem denseRange_iff_closure_range : DenseRange f ↔ closure (range f) = univ :=
  dense_iff_closure_eq

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