subset_closure_image_preimage_of_isOpen

English

If f has dense range and s is open in the codomain, then s is contained in the closure of f''(f^{-1}(s)).

Русский

Если образ f плотно насыщает пространство; для открытого s в кодо- Пространстве, тогда s ⊆ closure(f''(f^{-1}(s))).

LaTeX

$$$\\text{DenseRange}(f) \\to \\text{IsOpen}(s) \\Rightarrow s \\subseteq \\overline{f''(f^{-1}(s))}$$$

Lean4

/-- If `f` has dense range and `s` is an open set in the codomain of `f`, then the image of the
preimage of `s` under `f` is dense in `s`. -/
theorem subset_closure_image_preimage_of_isOpen (hf : DenseRange f) (hs : IsOpen s) : s ⊆ closure (f '' (f ⁻¹' s)) :=
  by
  rw [image_preimage_eq_inter_range]
  exact hf.open_subset_closure_inter hs

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