image_interior_subset — Mathlib

English

The image of the interior of s is contained in the interior of the image of s: f''(interior s) ⊆ interior(f''s).

Русский

Образ interior(s) находится внутри interior(f''s).

LaTeX

$$$$IsOpenMap(f) \\rightarrow \\forall s, f''(\\mathrm{interior}(s)) \\subseteq \\mathrm{interior}(f''s)$$$$

Lean4

theorem image_interior_subset (hf : IsOpenMap f) (s : Set X) : f '' interior s ⊆ interior (f '' s) :=
  (hf.mapsTo_interior (mapsTo_image f s)).image_subset

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