preimage_interior — Mathlib

English

For a homeomorphism h: X ≃ₜ Y and any subset s ⊆ Y, the preimage of the interior of s equals the interior of the preimage of s.

Русский

Для гомеоморфизма h: X ≃ₜ Y и подмножества s ⊆ Y имеет место h^{-1}(int(s)) = int(h^{-1}(s)).

LaTeX

$$$h^{-1}(\operatorname{int}(s)) = \operatorname{int}(h^{-1}(s)).$$$

Lean4

theorem preimage_interior (h : X ≃ₜ Y) (s : Set Y) : h ⁻¹' interior s = interior (h ⁻¹' s) :=
  h.isOpenMap.preimage_interior_eq_interior_preimage h.continuous _

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