preimage_frontier_eq_frontier_preimage

English

If f is open and continuous, then the preimage of the frontier equals the frontier of the preimage.

Русский

Если f открытое и непрерывное отображение, то f^{-1}(frontier s) = frontier(f^{-1}(s)).

LaTeX

$$$$IsOpenMap(f) \\rightarrow Continuous(f) \\rightarrow \\forall s, f^{-1}(\\mathrm{frontier}(s)) = \\mathrm{frontier}(f^{-1}(s))$$$$

Lean4

theorem preimage_frontier_eq_frontier_preimage (hf : IsOpenMap f) (hfc : Continuous f) (s : Set Y) :
    f ⁻¹' frontier s = frontier (f ⁻¹' s) := by
  simp only [frontier_eq_closure_inter_closure, preimage_inter, preimage_compl,
    hf.preimage_closure_eq_closure_preimage hfc]

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