coborder_preimage — Mathlib

English

If f is an open embedding, then coborder preimage commutes: coborder(f^{-1} s) = f^{-1} coborder s for all s.

Русский

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

LaTeX

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

Lean4

protected theorem coborder_preimage (hf : IsOpenEmbedding f) (s : Set Y) : coborder (f ⁻¹' s) = f ⁻¹' coborder s :=
  coborder_preimage hf.isOpenMap hf.continuous s

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