coborder_preimage_subset — Mathlib

English

If f is an open map, then for every s, coborder(f^{-1}(s)) ⊆ f^{-1}(coborder(s)).

Русский

Если f является открытым отображением, то для любого s верно coborder(f^{-1}(s)) ⊆ f^{-1}(coborder(s)).

LaTeX

$$$\operatorname{coborder}(f^{-1}(s)) \subseteq f^{-1}(\operatorname{coborder}(s))$$$

Lean4

theorem coborder_preimage_subset (hf : IsOpenMap f) (s : Set Y) : coborder (f ⁻¹' s) ⊆ f ⁻¹' (coborder s) :=
  by
  rw [coborder, coborder, preimage_compl, preimage_diff, compl_subset_compl]
  apply diff_subset_diff_left
  exact hf.preimage_closure_subset_closure_preimage

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