mapsTo_interior — Mathlib

English

If f maps s into t, then f maps interior s into interior t.

Русский

Если f отправляет множество s в множество t, то f отправляет interior(s) в interior(t).

LaTeX

$$$$IsOpenMap(f) \\rightarrow \\forall s,t, MapsTo(f,s,t) \\rightarrow MapsTo(f,\\mathrm{interior}(s),\\mathrm{interior}(t))$$$$

Lean4

theorem mapsTo_interior (hf : IsOpenMap f) {s : Set X} {t : Set Y} (h : MapsTo f s t) :
    MapsTo f (interior s) (interior t) :=
  mapsTo_iff_image_subset.2 <| interior_maximal (h.mono interior_subset Subset.rfl).image_subset (hf _ isOpen_interior)

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