preimage_coborder_subset — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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