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