dense_image — Mathlib

English

DenseRange f iff the closure of range f equals the universal set.

Русский

Плотность диапазона f эквивалентна тому, что замыкание образа f равно всему пространству.

LaTeX

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

Lean4

/-- The image of a dense set under a continuous map with dense range is a dense set. -/
theorem dense_image {f : X → Y} (hf' : DenseRange f) (hf : Continuous f) (hs : Dense s) : Dense (f '' s) :=
  (hf'.mono <| hf.range_subset_closure_image_dense hs).of_closure

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