preimage_interior_subset_interior_preimage

English

For any continuous f, the preimage of the interior of t is contained in the interior of the preimage of t.

Русский

Для непрерывной f предобраз внутренности t включается в внутренность предобраза t.

LaTeX

$$$\\text{Continuous}(f) \\Rightarrow f^{-1}(\\operatorname{Int}(t)) \\subseteq \\operatorname{Int}(f^{-1}(t))$$$

Lean4

/-- See also `interior_preimage_subset_preimage_interior`. -/
theorem preimage_interior_subset_interior_preimage {t : Set Y} (hf : Continuous f) :
    f ⁻¹' interior t ⊆ interior (f ⁻¹' t) :=
  interior_maximal (preimage_mono interior_subset) (isOpen_interior.preimage hf)

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