preimage_frontier_subset_frontier_preimage

English

Open map implies preimage of frontier is contained in frontier of preimage.

Русский

Открытое отображение не хуже: прообраз границы множества содержится в границе прообраза.

LaTeX

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

Lean4

theorem preimage_frontier_subset_frontier_preimage (hf : IsOpenMap f) {s : Set Y} :
    f ⁻¹' frontier s ⊆ frontier (f ⁻¹' s) := by
  simpa only [frontier_eq_closure_inter_closure, preimage_inter] using
    inter_subset_inter hf.preimage_closure_subset_closure_preimage hf.preimage_closure_subset_closure_preimage

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