range_subset_closure_image_dense — Mathlib

English

If f has dense range and is continuous, and s is dense, then the image f''s is dense.

Русский

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

LaTeX

$$$\\text{DenseRange}(f) \\land \\text{Continuous}(f) \\land \\text{Dense}(s) \\Rightarrow \\text{Dense}(f''s)$$$

Lean4

theorem range_subset_closure_image_dense {f : X → Y} (hf : Continuous f) (hs : Dense s) : range f ⊆ closure (f '' s) :=
  by
  rw [← image_univ, ← hs.closure_eq]
  exact image_closure_subset_closure_image hf

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