dense_of_mapsTo — Mathlib

English

If f has dense range and is continuous, and s is dense, and MapsTo f s t, then t is dense.

Русский

Если f имеет плотный диапазон и непрерывна, и s плотна, и MapsTo f s t, то t плотен.

LaTeX

$$$\\text{DenseRange}(f) \\land \\text{Continuous}(f) \\land \\text{Dense}(s) \\Rightarrow \\forall t,\\ \\text{MapsTo}(f,s,t) \\Rightarrow \\text{Dense}(t)$$$

Lean4

/-- If a continuous map with dense range maps a dense set to a subset of `t`, then `t` is a dense
set. -/
theorem dense_of_mapsTo {f : X → Y} (hf' : DenseRange f) (hf : Continuous f) (hs : Dense s) {t : Set Y}
    (ht : MapsTo f s t) : Dense t :=
  (hf'.dense_image hf hs).mono ht.image_subset

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