preimage_interior_subset_interior_preimage

English

The preimage of the interior of t intersected with s is contained in s intersect the interior of f^{-1}(t).

Русский

Предобраз внутренности t пересечённого с s содержится в s ∩ interior(f^{-1}(t)).

LaTeX

$$$s \\cap f^{-1}(\\mathrm{interior}(t)) \\subseteq s \\cap \\mathrm{interior}(f^{-1}(t))$$$

Lean4

theorem preimage_interior_subset_interior_preimage {t : Set β} (hf : ContinuousOn f s) (hs : IsOpen s) :
    s ∩ f ⁻¹' interior t ⊆ s ∩ interior (f ⁻¹' t) :=
  calc
    s ∩ f ⁻¹' interior t ⊆ interior (s ∩ f ⁻¹' t) :=
      interior_maximal (inter_subset_inter (Subset.refl _) (preimage_mono interior_subset))
        (hf.isOpen_inter_preimage hs isOpen_interior)
    _ = s ∩ interior (f ⁻¹' t) := by rw [interior_inter, hs.interior_eq]

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