image_interior — Mathlib

English

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

Русский

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

LaTeX

$$$h(\operatorname{int}(s)) = \operatorname{int}(h''s).$$$

Lean4

theorem image_interior (h : X ≃ₜ Y) (s : Set X) : h '' interior s = interior (h '' s) := by
  rw [← preimage_symm, preimage_interior]

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