image_closure — Mathlib

English

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

Русский

Для гомеоморфизма h: X ≃ₜ Y и подмножества s ⊆ X образ замыкания s равен замыканию образа s.

LaTeX

$$$h''\overline{s} = \overline{h''s}.$$$

Lean4

theorem image_closure (h : X ≃ₜ Y) (s : Set X) : h '' closure s = closure (h '' s) := by
  rw [← preimage_symm, preimage_closure]

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