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)