frontier_preimage_subset — Mathlib

English

If f is continuous, then the frontier (boundary) of the preimage is contained in the preimage of the frontier.

Русский

Если f непрерывна, граница предобраза включена в предобраз границы.

LaTeX

$$$\\operatorname{frontier}(f^{-1}(t)) \\subseteq f^{-1}(\\operatorname{frontier}(t))$$$

Lean4

theorem frontier_preimage_subset (hf : Continuous f) (t : Set Y) : frontier (f ⁻¹' t) ⊆ f ⁻¹' frontier t :=
  diff_subset_diff (hf.closure_preimage_subset t) (preimage_interior_subset_interior_preimage hf)

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