preimage_frontier — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem preimage_frontier (h : X ≃ₜ Y) (s : Set Y) : h ⁻¹' frontier s = frontier (h ⁻¹' s) :=
  h.isOpenMap.preimage_frontier_eq_frontier_preimage h.continuous _

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