interior_preimage_subset_preimage_interior

English

If f is open, then the interior of the preimage is contained in the preimage of the interior.

Русский

Если f открытое отображение, то interior(f^{-1}(s)) ⊆ f^{-1}(interior(s)).

LaTeX

$$$$IsOpenMap(f) \\rightarrow \\forall s, \\mathrm{interior}(f^{-1}(s)) \\subseteq f^{-1}(\\mathrm{interior}(s))$$$$

Lean4

theorem interior_preimage_subset_preimage_interior (hf : IsOpenMap f) {s : Set Y} :
    interior (f ⁻¹' s) ⊆ f ⁻¹' interior s :=
  hf.mapsTo_interior (mapsTo_preimage _ _)

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