coborder_preimage — Mathlib

English

For an open map and a continuous map f, coborder(f^{-1}(s)) equals f^{-1}(coborder(s)).

Русский

Для открытого отображения и непрерывного f выполняется coborder(f^{-1}(s)) = f^{-1}(coborder(s)).

LaTeX

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

Lean4

theorem coborder_preimage (hf : IsOpenMap f) (hf' : Continuous f) (s : Set Y) :
    coborder (f ⁻¹' s) = f ⁻¹' (coborder s) :=
  (hf.coborder_preimage_subset s).antisymm (hf'.preimage_coborder_subset s)

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