preimage_interior_eq_interior_preimage

English

If f is open and continuous, then the preimage of the interior equals the interior of the preimage.

Русский

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

LaTeX

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

Lean4

theorem preimage_interior_eq_interior_preimage (hf₁ : IsOpenMap f) (hf₂ : Continuous f) (s : Set Y) :
    f ⁻¹' interior s = interior (f ⁻¹' s) :=
  Subset.antisymm (preimage_interior_subset_interior_preimage hf₂) (interior_preimage_subset_preimage_interior hf₁)

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