preimage_closure — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem preimage_closure (h : X ≃ₜ Y) (s : Set Y) : h ⁻¹' closure s = closure (h ⁻¹' s) :=
  h.isOpenMap.preimage_closure_eq_closure_preimage h.continuous _

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